diff options
author | 2012-05-29 11:08:26 +0000 | |
---|---|---|
committer | 2012-05-29 11:08:26 +0000 | |
commit | 45038a0bfd5621153ba0dd4b6e06755fd15da1e3 (patch) | |
tree | 8a30a206d390e1b7450889189596641e5026ee46 /plugins/decl_mode/decl_interp.ml | |
parent | 3854ae16ffbaf56b90fbb85bcce3d92cd65ea6a6 (diff) |
Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15371 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/decl_mode/decl_interp.ml')
-rw-r--r-- | plugins/decl_mode/decl_interp.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 21d2b125e..a1e968668 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -185,7 +185,7 @@ let interp_constr_or_thesis check_sort sigma env = function let abstract_one_hyp inject h glob = match h with Hvar (loc,(id,None)) -> - GProd (dummy_loc,Name id, Explicit, GHole (loc,Evd.BinderType (Name id)), glob) + GProd (dummy_loc,Name id, Explicit, GHole (loc,Evar_kinds.BinderType (Name id)), glob) | Hvar (loc,(id,Some typ)) -> GProd (dummy_loc,Name id, Explicit, fst typ, glob) | Hprop st -> @@ -243,7 +243,7 @@ let rec glob_of_pat = let rec add_params n q = if n<=0 then q else add_params (pred n) (GHole(dummy_loc, - Evd.TomatchTypeParameter(ind,n))::q) in + Evar_kinds.TomatchTypeParameter(ind,n))::q) in let args = List.map glob_of_pat lpat in glob_app(loc,GRef(dummy_loc,Libnames.ConstructRef cstr), add_params mind.Declarations.mind_nparams args) @@ -252,14 +252,14 @@ let prod_one_hyp = function (loc,(id,None)) -> (fun glob -> GProd (dummy_loc,Name id, Explicit, - GHole (loc,Evd.BinderType (Name id)), glob)) + GHole (loc,Evar_kinds.BinderType (Name id)), glob)) | (loc,(id,Some typ)) -> (fun glob -> GProd (dummy_loc,Name id, Explicit, fst typ, glob)) let prod_one_id (loc,id) glob = GProd (dummy_loc,Name id, Explicit, - GHole (loc,Evd.BinderType (Name id)), glob) + GHole (loc,Evar_kinds.BinderType (Name id)), glob) let let_in_one_alias (id,pat) glob = GLetIn (dummy_loc,Name id, glob_of_pat pat, glob) @@ -339,7 +339,8 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = (fun (loc,(id,_)) -> GVar (loc,id)) params in let dum_args= - list_tabulate (fun _ -> GHole (dummy_loc,Evd.QuestionMark (Evd.Define false))) + list_tabulate + (fun _ -> GHole (dummy_loc,Evar_kinds.QuestionMark (Evar_kinds.Define false))) oib.Declarations.mind_nrealargs in glob_app(dummy_loc,rind,rparams@rparams_rec@dum_args) in let pat_vars,aliases,patt = interp_pattern env pat in @@ -415,7 +416,7 @@ let abstract_one_arg = function (loc,(id,None)) -> (fun glob -> GLambda (dummy_loc,Name id, Explicit, - GHole (loc,Evd.BinderType (Name id)), glob)) + GHole (loc,Evar_kinds.BinderType (Name id)), glob)) | (loc,(id,Some typ)) -> (fun glob -> GLambda (dummy_loc,Name id, Explicit, fst typ, glob)) |