diff options
| author | msozeau | 2006-03-22 15:36:58 +0000 |
|---|---|---|
| committer | msozeau | 2006-03-22 15:36:58 +0000 |
| commit | 10961655cb9c09da20cfe2ecc68def3d3b7d1bb5 (patch) | |
| tree | fe435d1bd014a15e0b430cac8d7fb6bddc75f5e3 /interp | |
| parent | 8291c83620312550d1ccbe9a304fd43f35724b12 (diff) | |
Made pretyping a functor over a coercion implementation. Pretyping.Default uses the original Coercion implementation.
Updated contributions that called pretyping to use the default impl.
Also update subtac using the functor, do some renamings and add interfaces for all files.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8654 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index bda43f8121..2057eb5b27 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -18,6 +18,7 @@ open Impargs open Rawterm open Pattern open Pretyping +open Cases open Topconstr open Nametab open Notation @@ -387,12 +388,12 @@ let check_constructor_length env loc cstr pl pl0 = let nargs = Inductiveops.constructor_nrealargs env cstr in let nhyps = Inductiveops.constructor_nrealhyps env cstr in if n <> nargs && n <> nhyps (* i.e. with let's *) then - Cases.error_wrong_numarg_constructor_loc loc env cstr nargs + error_wrong_numarg_constructor_loc loc env cstr nargs let check_inductive_length env (loc,ind,nal) = let n = Inductiveops.inductive_nargs env ind in if n <> List.length nal then - Cases.error_wrong_numarg_inductive_loc loc env ind n + error_wrong_numarg_inductive_loc loc env ind n (* Manage multiple aliases *) @@ -1068,7 +1069,7 @@ let intern_ltac isarity ltacvars sigma env c = let interp_gen kind sigma env ?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[])) c = - understand_gen kind sigma env + Default.understand_gen kind sigma env (intern_gen (kind=IsType) ~impls ~allow_soapp ~ltacvars sigma env c) let interp_constr sigma env c = @@ -1081,10 +1082,10 @@ let interp_casted_constr sigma env ?(impls=([],[])) c typ = interp_gen (OfType (Some typ)) sigma env ~impls c let interp_open_constr sigma env c = - understand_tcc sigma env (intern_constr sigma env c) + Default.understand_tcc sigma env (intern_constr sigma env c) let interp_constr_judgment sigma env c = - understand_judgment sigma env (intern_constr sigma env c) + Default.understand_judgment sigma env (intern_constr sigma env c) type ltac_sign = identifier list * unbound_ltac_var_map @@ -1109,7 +1110,7 @@ let interp_aconstr impls vars a = let interp_binder sigma env na t = let t = intern_gen true sigma env t in - understand_type sigma env (locate_if_isevar (loc_of_rawconstr t) na t) + Default.understand_type sigma env (locate_if_isevar (loc_of_rawconstr t) na t) open Environ open Term |