diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-12 14:41:00 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-12 14:41:00 +0000 |
| commit | fd8b1d101c07c69252719e9e35209baf019216be (patch) | |
| tree | f966da5805fffc8cef5dfcecf0000943ea5eecbc | |
| parent | 7dfc58207fc6a1eb50841640fb26aa8e32ca17c7 (diff) | |
Scope type pour le codomaine de Prod aussi; ajout extern_rawtype
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4360 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | interp/constrextern.ml | 6 | ||||
| -rw-r--r-- | interp/constrextern.mli | 1 |
2 files changed, 5 insertions, 2 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 7b07e0a96..d940aae37 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -20,7 +20,6 @@ open Inductive open Sign open Environ open Libnames -open Declare open Impargs open Topconstr open Rawterm @@ -573,7 +572,7 @@ and factorize_prod scopes vars aty = function -> let id = avoid_wildcard id in let (nal,c) = factorize_prod scopes (Idset.add id vars) aty c in ((loc,Name id)::nal,c) - | c -> ([],extern true scopes vars c) + | c -> ([],extern_type scopes vars c) and factorize_lambda inctx scopes vars aty = function | RLambda (loc,na,ty,c) @@ -637,6 +636,9 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function let extern_rawconstr vars c = extern false (None,Symbols.current_scopes()) vars c +let extern_rawtype vars c = + extern_type (None,Symbols.current_scopes()) vars c + let extern_cases_pattern vars p = extern_cases_pattern_in_scope (Symbols.current_scopes()) vars p diff --git a/interp/constrextern.mli b/interp/constrextern.mli index c5595f5a9..d088867c5 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -33,6 +33,7 @@ val check_same_type : constr_expr -> constr_expr -> unit val extern_cases_pattern : Idset.t -> cases_pattern -> cases_pattern_expr val extern_rawconstr : Idset.t -> rawconstr -> constr_expr +val extern_rawtype : Idset.t -> rawconstr -> constr_expr val extern_pattern : env -> names_context -> constr_pattern -> constr_expr (* If [b=true] in [extern_constr b env c] then the variables in the first |