From 45038a0bfd5621153ba0dd4b6e06755fd15da1e3 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 29 May 2012 11:08:26 +0000 Subject: 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 --- plugins/decl_mode/decl_interp.ml | 13 +++++++------ plugins/decl_mode/decl_proof_instr.ml | 7 +++++-- plugins/firstorder/instances.ml | 2 +- plugins/funind/glob_termops.ml | 2 +- plugins/syntax/numbers_syntax.ml | 4 ++-- 5 files changed, 16 insertions(+), 12 deletions(-) (limited to 'plugins') 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)) diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index c848faaa7..2870e8f7e 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -1288,8 +1288,11 @@ let understand_my_constr c gls = let env = pf_env gls in let nc = names_of_rel_context env in let rawc = Detyping.detype false [] nc c in - let rec frob = function GEvar _ -> GHole (dummy_loc,QuestionMark Expand) | rc -> map_glob_constr frob rc in - Pretyping.understand_tcc (sig_sig gls) env ~expected_type:(pf_concl gls) (frob rawc) + let rec frob = function + | GEvar _ -> GHole (dummy_loc,Evar_kinds.QuestionMark Evar_kinds.Expand) + | rc -> map_glob_constr frob rc + in + Pretyping.understand_tcc (sig_sig gls) env ~expected_type:(pf_concl gls) (frob rawc) let my_refine c gls = let oc = understand_my_constr c gls in diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index a955891f8..8d580d235 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -127,7 +127,7 @@ let mk_open_instance id gl m t= match t with GLambda(loc,name,k,_,t0)-> let t1=raux (n-1) t0 in - GLambda(loc,name,k,GHole (dummy_loc,Evd.BinderType name),t1) + GLambda(loc,name,k,GHole (dummy_loc,Evar_kinds.BinderType name),t1) | _-> anomaly "can't happen" in let ntt=try Pretyping.understand evmap env (raux m rawt) diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index b458346d4..b14197891 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -18,7 +18,7 @@ let mkGProd(n,t,b) = GProd(dummy_loc,n,Explicit,t,b) let mkGLetIn(n,t,b) = GLetIn(dummy_loc,n,t,b) let mkGCases(rto,l,brl) = GCases(dummy_loc,Term.RegularStyle,rto,l,brl) let mkGSort s = GSort(dummy_loc,s) -let mkGHole () = GHole(dummy_loc,Evd.BinderType Anonymous) +let mkGHole () = GHole(dummy_loc,Evar_kinds.BinderType Anonymous) let mkGCast(b,t) = GCast(dummy_loc,b,CastConv (Term.DEFAULTcast,t)) (* diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml index cbc8d7fd6..984bae418 100644 --- a/plugins/syntax/numbers_syntax.ml +++ b/plugins/syntax/numbers_syntax.ml @@ -180,10 +180,10 @@ let word_of_pos_bigint dloc hght n = if is_neg_or_zero hgt then int31_of_pos_bigint dloc n else if equal n zero then - GApp (dloc, ref_W0, [GHole (dloc, Evd.InternalHole)]) + GApp (dloc, ref_W0, [GHole (dloc, Evar_kinds.InternalHole)]) else let (h,l) = split_at hgt n in - GApp (dloc, ref_WW, [GHole (dloc, Evd.InternalHole); + GApp (dloc, ref_WW, [GHole (dloc, Evar_kinds.InternalHole); decomp (sub_1 hgt) h; decomp (sub_1 hgt) l]) in -- cgit v1.2.3