diff options
43 files changed, 217 insertions, 197 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index d0e26b3ba..2e74b809f 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -997,7 +997,7 @@ let extern_sort s = extern_glob_sort (detype_sort s) let any_any_branch = (* | _ => _ *) - (loc,[],[PatVar (loc,Anonymous)],GHole (loc,Evd.InternalHole)) + (loc,[],[PatVar (loc,Anonymous)],GHole (loc,Evar_kinds.InternalHole)) let rec glob_of_pat env = function | PRef ref -> GRef (loc,ref) @@ -1010,7 +1010,7 @@ let rec glob_of_pat env = function anomaly "glob_constr_of_pattern: index to an anonymous variable" with Not_found -> id_of_string ("_UNBOUND_REL_"^(string_of_int n)) in GVar (loc,id) - | PMeta None -> GHole (loc,Evd.InternalHole) + | PMeta None -> GHole (loc,Evar_kinds.InternalHole) | PMeta (Some n) -> GPatVar (loc,(false,n)) | PApp (f,args) -> GApp (loc,glob_of_pat env f,array_map_to_list (glob_of_pat env) args) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 6a9b07410..af48a37c9 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -362,7 +362,7 @@ let locate_if_isevar loc na = function (try match na with | Name id -> glob_constr_of_aconstr loc (Reserve.find_reserved_type id) | Anonymous -> raise Not_found - with Not_found -> GHole (loc, Evd.BinderType na)) + with Not_found -> GHole (loc, Evar_kinds.BinderType na)) | x -> x let reset_hidden_inductive_implicit_test env = @@ -406,7 +406,11 @@ let intern_generalized_binder ?(global_level=false) intern_type lvar let env' = List.fold_left (fun env (x, l) -> push_name_env ~global_level lvar (Variable,[],[],[])(*?*) env (l, Name x)) env fvs in - let bl = List.map (fun (id, loc) -> (loc, (Name id, b, None, GHole (loc, Evd.BinderType (Name id))))) fvs in + let bl = List.map + (fun (id, loc) -> + (loc, (Name id, b, None, GHole (loc, Evar_kinds.BinderType (Name id))))) + fvs + in let na = match na with | Anonymous -> if global_level then na @@ -444,7 +448,7 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio | LocalRawDef((loc,na as locna),def) -> let indef = intern env def in (push_name_env lvar (impls_term_list indef) env locna, - (loc,(na,Explicit,Some(indef),GHole(loc,Evd.BinderType na)))::bl) + (loc,(na,Explicit,Some(indef),GHole(loc,Evar_kinds.BinderType na)))::bl) let intern_generalization intern env lvar loc bk ak c = let c = intern {env with unb = true} c in @@ -460,10 +464,10 @@ let intern_generalization intern env lvar loc bk ak c = in if pi then (fun (id, loc') acc -> - GProd (join_loc loc' loc, Name id, bk, GHole (loc', Evd.BinderType (Name id)), acc)) + GProd (join_loc loc' loc, Name id, bk, GHole (loc', Evar_kinds.BinderType (Name id)), acc)) else (fun (id, loc') acc -> - GLambda (join_loc loc' loc, Name id, bk, GHole (loc', Evd.BinderType (Name id)), acc)) + GLambda (join_loc loc' loc, Name id, bk, GHole (loc', Evar_kinds.BinderType (Name id)), acc)) in List.fold_right (fun (id, loc as lid) (env, acc) -> let env' = push_name_env lvar (Variable,[],[],[]) env (loc, Name id) in @@ -549,11 +553,11 @@ let subst_aconstr_in_glob_constr loc intern lvar subst infos c = (if lassoc then List.rev l else l) termin with Not_found -> anomaly "Inconsistent substitution of recursive notation") - | AHole (Evd.BinderType (Name id as na)) -> + | AHole (Evar_kinds.BinderType (Name id as na)) -> let na = try snd (coerce_to_name (fst (List.assoc id terms))) with Not_found -> na in - GHole (loc,Evd.BinderType na) + GHole (loc,Evar_kinds.BinderType na) | ABinderList (x,_,iter,terminator) -> (try (* All elements of the list are in scopes (scopt,subscopes) *) @@ -1266,8 +1270,8 @@ let get_implicit_name n imps = Some (Impargs.name_of_implicit (List.nth imps (n-1))) let set_hole_implicit i b = function - | GRef (loc,r) | GApp (_,GRef (loc,r),_) -> (loc,Evd.ImplicitArg (r,i,b)) - | GVar (loc,id) -> (loc,Evd.ImplicitArg (VarRef id,i,b)) + | GRef (loc,r) | GApp (_,GRef (loc,r),_) -> (loc,Evar_kinds.ImplicitArg (r,i,b)) + | GVar (loc,id) -> (loc,Evar_kinds.ImplicitArg (VarRef id,i,b)) | _ -> anomaly "Only refs have implicits" let exists_implicit_name id = @@ -1440,7 +1444,7 @@ let internalize sigma globalenv env allow_patvar lvar c = | CRecord (loc, _, fs) -> let cargs = sort_fields true loc fs - (fun k l -> CHole (loc, Some (Evd.QuestionMark (Evd.Define true))) :: l) + (fun k l -> CHole (loc, Some (Evar_kinds.QuestionMark (Evar_kinds.Define true))) :: l) in begin match cargs with @@ -1478,9 +1482,9 @@ let internalize sigma globalenv env allow_patvar lvar c = GCases(dummy_loc,Term.RegularStyle,Some (GSort (dummy_loc,GType None)), (* "return Type" *) List.map (fun id -> GVar (dummy_loc,id),(Name id,None)) thevars, (* "match v1,..,vn" *) [dummy_loc,[],thepats, (* "|p1,..,pn" *) - Option.cata (intern_type env') (GHole(dummy_loc,Evd.CasesType)) rtnpo; (* "=> P" is there were a P "=> _" else *) + Option.cata (intern_type env') (GHole(dummy_loc,Evar_kinds.CasesType)) rtnpo; (* "=> P" is there were a P "=> _" else *) dummy_loc,[],list_make (List.length thepats) (PatVar(dummy_loc,Anonymous)), (* "|_,..,_" *) - GHole(dummy_loc,Evd.ImpossibleCase) (* "=> _" *)])) + GHole(dummy_loc,Evar_kinds.ImpossibleCase) (* "=> _" *)])) in let eqns' = List.map (intern_eqn (List.length tms) env) eqns in GCases (loc, sty, rtnpo, tms, List.flatten eqns') @@ -1503,7 +1507,7 @@ let internalize sigma globalenv env allow_patvar lvar c = intern_type env'' p) po in GIf (loc, c', (na', p'), intern env b1, intern env b2) | CHole (loc, k) -> - GHole (loc, match k with Some k -> k | None -> Evd.QuestionMark (Evd.Define true)) + GHole (loc, match k with Some k -> k | None -> Evar_kinds.QuestionMark (Evar_kinds.Define true)) | CPatVar (loc, n) when allow_patvar -> GPatVar (loc, n) | CPatVar (loc, _) -> diff --git a/interp/reserve.ml b/interp/reserve.ml index 7f30c6bac..c3cdd3f72 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -94,7 +94,7 @@ let anonymize_if_reserved na t = match na with if not !Flags.raw_print & (try aconstr_of_glob_constr [] [] t = find_reserved_type id with UserError _ -> false) - then GHole (dummy_loc,Evd.BinderType na) + then GHole (dummy_loc,Evar_kinds.BinderType na) else t with Not_found -> t) | Anonymous -> t diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 9cad91068..1a86170f3 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -31,7 +31,7 @@ type aconstr = | ARef of global_reference | AVar of identifier | AApp of aconstr * aconstr list - | AHole of Evd.hole_kind + | AHole of Evar_kinds.t | AList of identifier * identifier * aconstr * aconstr * bool (* Part only in glob_constr *) | ALambda of name * aconstr * aconstr @@ -485,13 +485,14 @@ let rec subst_aconstr subst bound raw = | APatVar _ | ASort _ -> raw - | AHole (Evd.ImplicitArg (ref,i,b)) -> + | AHole (Evar_kinds.ImplicitArg (ref,i,b)) -> let ref',t = subst_global subst ref in if ref' == ref then raw else - AHole (Evd.InternalHole) - | AHole (Evd.BinderType _ | Evd.QuestionMark _ | Evd.CasesType - | Evd.InternalHole | Evd.TomatchTypeParameter _ | Evd.GoalEvar - | Evd.ImpossibleCase | Evd.MatchingVar _) -> raw + AHole (Evar_kinds.InternalHole) + | AHole (Evar_kinds.BinderType _ |Evar_kinds.QuestionMark _ + |Evar_kinds.CasesType |Evar_kinds.InternalHole + |Evar_kinds.TomatchTypeParameter _ |Evar_kinds.GoalEvar + |Evar_kinds.ImpossibleCase |Evar_kinds.MatchingVar _) -> raw | ACast (r1,k) -> match k with @@ -521,11 +522,12 @@ let abstract_return_type_context pi mklam tml rtno = let abstract_return_type_context_glob_constr = abstract_return_type_context (fun (_,_,nal) -> nal) - (fun na c -> GLambda(dummy_loc,na,Explicit,GHole(dummy_loc,Evd.InternalHole),c)) + (fun na c -> + GLambda(dummy_loc,na,Explicit,GHole(dummy_loc,Evar_kinds.InternalHole),c)) let abstract_return_type_context_aconstr = abstract_return_type_context snd - (fun na c -> ALambda(na,AHole Evd.InternalHole,c)) + (fun na c -> ALambda(na,AHole Evar_kinds.InternalHole,c)) exception No_match @@ -568,7 +570,7 @@ let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with | (_,Name id2) when List.mem id2 (fst metas) -> let rhs = match na1 with | Name id1 -> GVar (dummy_loc,id1) - | Anonymous -> GHole (dummy_loc,Evd.InternalHole) in + | Anonymous -> GHole (dummy_loc,Evar_kinds.InternalHole) in alp, bind_env alp sigma id2 rhs | (Name id1,Name id2) -> (id1,id2)::alp,sigma | (Anonymous,Anonymous) -> alp,sigma @@ -592,7 +594,7 @@ let rec match_iterated_binders islambda decls = function match_iterated_binders islambda ((na,bk,None,t)::decls) b | GLetIn (loc,na,c,b) when glue_letin_with_decls -> match_iterated_binders islambda - ((na,Explicit (*?*), Some c,GHole(loc,Evd.BinderType na))::decls) b + ((na,Explicit (*?*), Some c,GHole(loc,Evar_kinds.BinderType na))::decls) b | b -> (decls,b) let remove_sigma x (sigmavar,sigmalist,sigmabinders) = @@ -742,7 +744,7 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 = | b1, ALambda (Name id,AHole _,b2) when inner -> let id' = Namegen.next_ident_away id (free_glob_vars b1) in match_in u alp metas (bind_binder sigma id - [(Name id',Explicit,None,GHole(dummy_loc,Evd.BinderType (Name id')))]) + [(Name id',Explicit,None,GHole(dummy_loc,Evar_kinds.BinderType (Name id')))]) (mkGApp dummy_loc b1 (GVar (dummy_loc,id'))) b2 | (GRec _ | GEvar _), _ @@ -905,7 +907,7 @@ type constr_expr = constr_expr * constr_expr | CIf of loc * constr_expr * (name located option * constr_expr option) * constr_expr * constr_expr - | CHole of loc * Evd.hole_kind option + | CHole of loc * Evar_kinds.t option | CPatVar of loc * (bool * patvar) | CEvar of loc * existential_key * constr_expr list option | CSort of loc * glob_sort diff --git a/interp/topconstr.mli b/interp/topconstr.mli index a7871d41b..48871432e 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -27,7 +27,7 @@ type aconstr = | ARef of global_reference | AVar of identifier | AApp of aconstr * aconstr list - | AHole of Evd.hole_kind + | AHole of Evar_kinds.t | AList of identifier * identifier * aconstr * aconstr * bool (** Part only in [glob_constr] *) | ALambda of name * aconstr * aconstr @@ -158,7 +158,7 @@ type constr_expr = constr_expr * constr_expr | CIf of loc * constr_expr * (name located option * constr_expr option) * constr_expr * constr_expr - | CHole of loc * Evd.hole_kind option + | CHole of loc * Evar_kinds.t option | CPatVar of loc * (bool * patvar) | CEvar of loc * existential_key * constr_expr list option | CSort of loc * glob_sort diff --git a/intf/evar_kinds.mli b/intf/evar_kinds.mli new file mode 100644 index 000000000..fae83ee95 --- /dev/null +++ b/intf/evar_kinds.mli @@ -0,0 +1,29 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names +open Libnames + +(** The kinds of existential variable *) + +(** Should the obligation be defined (opaque or transparent (default)) or + defined transparent and expanded in the term? *) + +type obligation_definition_status = Define of bool | Expand + +type t = + | ImplicitArg of global_reference * (int * identifier option) + * bool (** Force inference *) + | BinderType of name + | QuestionMark of obligation_definition_status + | CasesType + | InternalHole + | TomatchTypeParameter of inductive * int + | GoalEvar + | ImpossibleCase + | MatchingVar of bool * identifier diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index abd1607d6..06d922a7c 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -34,12 +34,12 @@ let mk_cast = function let binders_of_names l = List.map (fun (loc, na) -> LocalRawAssum ([loc, na], Default Explicit, - CHole (loc, Some (Evd.BinderType na)))) l + CHole (loc, Some (Evar_kinds.BinderType na)))) l let binders_of_lidents l = List.map (fun (loc, id) -> LocalRawAssum ([loc, Name id], Default Glob_term.Explicit, - CHole (loc, Some (Evd.BinderType (Name id))))) l + CHole (loc, Some (Evar_kinds.BinderType (Name id))))) l let mk_fixb (id,bl,ann,body,(loc,tyc)) = let ty = match tyc with diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4 index 5bd215190..f5225feb3 100644 --- a/parsing/q_constr.ml4 +++ b/parsing/q_constr.ml4 @@ -75,7 +75,7 @@ EXTEND | "0" [ s = sort -> <:expr< Glob_term.GSort ($dloc$,s) >> | id = ident -> <:expr< Glob_term.GVar ($dloc$,$id$) >> - | "_" -> <:expr< Glob_term.GHole ($dloc$, QuestionMark (Define False)) >> + | "_" -> <:expr< Glob_term.GHole ($dloc$,Evar_kinds.QuestionMark (Evar_kinds.Define False)) >> | "?"; id = ident -> <:expr< Glob_term.GPatVar($dloc$,(False,$id$)) >> | "{"; c1 = constr; "}"; "+"; "{"; c2 = constr; "}" -> apply_ref <:expr< coq_sumbool_ref >> [c1;c2] 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 diff --git a/pretyping/cases.ml b/pretyping/cases.ml index cc4b3f07f..7019495af 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -278,8 +278,8 @@ let rec find_row_ind = function let inductive_template evdref env tmloc ind = let arsign = get_full_arity_sign env ind in let hole_source = match tmloc with - | Some loc -> fun i -> (loc, TomatchTypeParameter (ind,i)) - | None -> fun _ -> (dummy_loc, InternalHole) in + | Some loc -> fun i -> (loc, Evar_kinds.TomatchTypeParameter (ind,i)) + | None -> fun _ -> (dummy_loc, Evar_kinds.InternalHole) in let (_,evarl,_) = List.fold_right (fun (na,b,ty) (subst,evarl,n) -> @@ -357,7 +357,7 @@ let coerce_to_indtype typing_fun evdref env matx tomatchl = (************************************************************************) (* Utils *) -let mkExistential env ?(src=(dummy_loc,InternalHole)) evdref = +let mkExistential env ?(src=(dummy_loc,Evar_kinds.InternalHole)) evdref = e_new_evar evdref env ~src:src (new_Type ()) let evd_comb2 f evdref x y = @@ -909,7 +909,7 @@ let expand_arg tms (p,ccl) ((_,t),_,na) = let adjust_impossible_cases pb pred tomatch submat = if submat = [] then match kind_of_term (whd_evar !(pb.evdref) pred) with - | Evar (evk,_) when snd (evar_source evk !(pb.evdref)) = ImpossibleCase -> + | Evar (evk,_) when snd (evar_source evk !(pb.evdref)) = Evar_kinds.ImpossibleCase -> let default = (coq_unit_judge ()).uj_type in pb.evdref := Evd.define evk default !(pb.evdref); (* we add an "assert false" case *) @@ -1469,7 +1469,7 @@ let abstract_tycon loc env evdref subst _tycon extenv t = (fun i _ -> try list_assoc_in_triple i subst0 with Not_found -> mkRel i) 1 (rel_context env) in - let ev = e_new_evar evdref env ~src:(loc, CasesType) ty in + let ev = e_new_evar evdref env ~src:(loc, Evar_kinds.CasesType) ty in evdref := add_conv_pb (Reduction.CONV,env,substl inst ev,t) !evdref; ev | _ -> @@ -1492,7 +1492,8 @@ let abstract_tycon loc env evdref subst _tycon extenv t = let filter = rel_filter@named_filter in let candidates = u :: List.map mkRel vl in let ev = - e_new_evar evdref extenv ~src:(loc, CasesType) ~filter ~candidates ty in + e_new_evar evdref extenv ~src:(loc, Evar_kinds.CasesType) + ~filter ~candidates ty in lift k ev else map_constr_with_full_binders push_binder aux x t in @@ -1507,7 +1508,7 @@ let build_tycon loc env tycon_env subst tycon extenv evdref t = let n' = rel_context_length (rel_context tycon_env) in let tt = new_Type () in let impossible_case_type = - e_new_evar evdref env ~src:(loc,ImpossibleCase) tt in + e_new_evar evdref env ~src:(loc,Evar_kinds.ImpossibleCase) tt in (lift (n'-n) impossible_case_type, tt) | Some t -> let t = abstract_tycon loc tycon_env evdref subst tycon extenv t in @@ -1759,7 +1760,7 @@ let prepare_predicate loc typing_fun sigma env tomatchs arsign tycon pred = (* we use two strategies *) let sigma,t = match tycon with | Some t -> sigma,t - | None -> new_type_evar sigma env ~src:(loc, CasesType) in + | None -> new_type_evar sigma env ~src:(loc, Evar_kinds.CasesType) in (* First strategy: we build an "inversion" predicate *) let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in (* Second strategy: we directly use the evar as a non dependent pred *) @@ -1825,7 +1826,7 @@ let mk_JMeq typ x typ' y = mkApp (delayed_force coq_JMeq_ind, [| typ; x ; typ'; y |]) let mk_JMeq_refl typ x = mkApp (delayed_force coq_JMeq_refl, [| typ; x |]) -let hole = GHole (dummy_loc, Evd.QuestionMark (Evd.Define true)) +let hole = GHole (dummy_loc, Evar_kinds.QuestionMark (Evar_kinds.Define true)) let constr_of_pat env isevars arsign pat avoid = let rec typ env (ty, realargs) pat avoid = diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 60e10ac8e..34eb92fa0 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -66,8 +66,8 @@ let inh_pattern_coerce_to loc pat ind1 ind2 = open Program -let make_existential loc ?(opaque = Define true) env isevars c = - Evarutil.e_new_evar isevars env ~src:(loc, QuestionMark opaque) c +let make_existential loc ?(opaque = Evar_kinds.Define true) env isevars c = + Evarutil.e_new_evar isevars env ~src:(loc, Evar_kinds.QuestionMark opaque) c let app_opt env evars f t = whd_betaiota !evars (app_opt f t) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 99d054e56..33e1ecdf2 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -658,13 +658,14 @@ let rec subst_glob_constr subst raw = | GSort _ -> raw - | GHole (loc,ImplicitArg (ref,i,b)) -> + | GHole (loc,Evar_kinds.ImplicitArg (ref,i,b)) -> let ref',_ = subst_global subst ref in if ref' == ref then raw else - GHole (loc,InternalHole) - | GHole (loc, (BinderType _ | QuestionMark _ | CasesType | InternalHole | - TomatchTypeParameter _ | GoalEvar | ImpossibleCase | MatchingVar _)) -> - raw + GHole (loc,Evar_kinds.InternalHole) + | GHole (loc, (Evar_kinds.BinderType _ |Evar_kinds.QuestionMark _ + |Evar_kinds.CasesType |Evar_kinds.InternalHole + |Evar_kinds.TomatchTypeParameter _ |Evar_kinds.GoalEvar + |Evar_kinds.ImpossibleCase |Evar_kinds.MatchingVar _)) -> raw | GCast (loc,r1,k) -> (match k with diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index cddfbd5d1..ab11df450 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -540,7 +540,7 @@ and conv_record trs env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) List.fold_left (fun (i,ks,m) b -> if m=n then (i,t2::ks, m-1) else - let dloc = (dummy_loc,InternalHole) in + let dloc = (dummy_loc,Evar_kinds.InternalHole) in let (i',ev) = new_evar i env ~src:dloc (substl ks b) in (i', ev :: ks, m - 1)) (evd,[],List.length bs - 1) bs @@ -816,7 +816,7 @@ let rec solve_unconstrained_evars_with_canditates evd = let solve_unconstrained_impossible_cases evd = Evd.fold_undefined (fun evk ev_info evd' -> match ev_info.evar_source with - | _,ImpossibleCase -> Evd.define evk (j_type (coq_unit_judge ())) evd' + | _,Evar_kinds.ImpossibleCase -> Evd.define evk (j_type (coq_unit_judge ())) evd' | _ -> evd') evd evd let consider_remaining_unif_problems ?(ts=full_transparent_state) env evd = diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index da99436ca..84a1cd550 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -308,7 +308,7 @@ let push_rel_context_to_named_context env typ = * Entry points to define new evars * *------------------------------------*) -let default_source = (dummy_loc,InternalHole) +let default_source = (dummy_loc,Evar_kinds.InternalHole) let new_pure_evar evd sign ?(src=default_source) ?filter ?candidates typ = let newevk = new_untyped_evar() in @@ -338,7 +338,7 @@ let new_type_evar ?src ?filter evd env = new_evar evd' env ?src ?filter (mkSort s) (* The same using side-effect *) -let e_new_evar evdref env ?(src=(dummy_loc,InternalHole)) ?filter ?candidates ty = +let e_new_evar evdref env ?(src=(dummy_loc,Evar_kinds.InternalHole)) ?filter ?candidates ty = let (evd',ev) = new_evar !evdref env ~src:src ?filter ?candidates ty in evdref := evd'; ev @@ -1874,7 +1874,7 @@ let check_evars env initial_sigma sigma c = if not (Evd.mem initial_sigma evk) then let (loc,k) = evar_source evk sigma in match k with - | ImplicitArg (gr, (i, id), false) -> () + | Evar_kinds.ImplicitArg (gr, (i, id), false) -> () | _ -> let evi = nf_evar_info sigma (Evd.find_undefined sigma evk) in error_unsolvable_implicit loc env sigma evi k None) diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index bef5398aa..82d154d39 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -30,18 +30,18 @@ val new_untyped_evar : unit -> existential_key (** {6 Creating a fresh evar given their type and context} *) val new_evar : - evar_map -> env -> ?src:loc * hole_kind -> ?filter:bool list -> + evar_map -> env -> ?src:loc * Evar_kinds.t -> ?filter:bool list -> ?candidates:constr list -> types -> evar_map * constr (** the same with side-effects *) val e_new_evar : - evar_map ref -> env -> ?src:loc * hole_kind -> ?filter:bool list -> + evar_map ref -> env -> ?src:loc * Evar_kinds.t -> ?filter:bool list -> ?candidates:constr list -> types -> constr (** Create a new Type existential variable, as we keep track of them during type-checking and unification. *) val new_type_evar : - ?src:loc * hole_kind -> ?filter:bool list -> evar_map -> env -> evar_map * constr + ?src:loc * Evar_kinds.t -> ?filter:bool list -> evar_map -> env -> evar_map * constr (** Create a fresh evar in a context different from its definition context: [new_evar_instance sign evd ty inst] creates a new evar of context @@ -50,7 +50,7 @@ val new_type_evar : of [inst] are typed in the occurrence context and their type (seen as a telescope) is [sign] *) val new_evar_instance : - named_context_val -> evar_map -> types -> ?src:loc * hole_kind -> ?filter:bool list -> ?candidates:constr list -> constr list -> evar_map * constr + named_context_val -> evar_map -> types -> ?src:loc * Evar_kinds.t -> ?filter:bool list -> ?candidates:constr list -> constr list -> evar_map * constr val make_pure_subst : evar_info -> constr array -> (identifier * constr) list diff --git a/pretyping/evd.ml b/pretyping/evd.ml index f1c278bd2..5164385ce 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -18,24 +18,11 @@ open Environ open Libnames open Mod_subst -(* The kinds of existential variable *) - -type obligation_definition_status = Define of bool | Expand - -type hole_kind = - | ImplicitArg of global_reference * (int * identifier option) * bool - | BinderType of name - | QuestionMark of obligation_definition_status - | CasesType - | InternalHole - | TomatchTypeParameter of inductive * int - | GoalEvar - | ImpossibleCase - | MatchingVar of bool * identifier +(* The kinds of existential variables are now defined in [Evar_kinds] *) (* The type of mappings for existential variables *) -type evar = existential_key +type evar = Term.existential_key let string_of_existential evk = "?" ^ string_of_int evk let existential_of_int evk = evk @@ -49,7 +36,7 @@ type evar_info = { evar_hyps : named_context_val; evar_body : evar_body; evar_filter : bool list; - evar_source : hole_kind located; + evar_source : Evar_kinds.t located; evar_candidates : constr list option; (* if not None, list of allowed instances *) evar_extra : Store.t } @@ -58,7 +45,7 @@ let make_evar hyps ccl = { evar_hyps = hyps; evar_body = Evar_empty; evar_filter = List.map (fun _ -> true) (named_context_of_val hyps); - evar_source = (dummy_loc,InternalHole); + evar_source = (dummy_loc,Evar_kinds.InternalHole); evar_candidates = None; evar_extra = Store.empty } @@ -432,7 +419,7 @@ let define evk body evd = | [] -> evd.last_mods | _ -> ExistentialSet.add evk evd.last_mods } -let evar_declare hyps evk ty ?(src=(dummy_loc,InternalHole)) ?filter ?candidates evd = +let evar_declare hyps evk ty ?(src=(dummy_loc,Evar_kinds.InternalHole)) ?filter ?candidates evd = let filter = if filter = None then List.map (fun _ -> true) (named_context_of_val hyps) @@ -752,20 +739,20 @@ let pr_decl ((id,b,_),ok) = print_constr c ++ str (if ok then ")" else "}") let pr_evar_source = function - | QuestionMark _ -> str "underscore" - | CasesType -> str "pattern-matching return predicate" - | BinderType (Name id) -> str "type of " ++ Nameops.pr_id id - | BinderType Anonymous -> str "type of anonymous binder" - | ImplicitArg (c,(n,ido),b) -> + | Evar_kinds.QuestionMark _ -> str "underscore" + | Evar_kinds.CasesType -> str "pattern-matching return predicate" + | Evar_kinds.BinderType (Name id) -> str "type of " ++ Nameops.pr_id id + | Evar_kinds.BinderType Anonymous -> str "type of anonymous binder" + | Evar_kinds.ImplicitArg (c,(n,ido),b) -> let id = Option.get ido in str "parameter " ++ pr_id id ++ spc () ++ str "of" ++ spc () ++ print_constr (constr_of_global c) - | InternalHole -> str "internal placeholder" - | TomatchTypeParameter (ind,n) -> + | Evar_kinds.InternalHole -> str "internal placeholder" + | Evar_kinds.TomatchTypeParameter (ind,n) -> pr_nth n ++ str " argument of type " ++ print_constr (mkInd ind) - | GoalEvar -> str "goal evar" - | ImpossibleCase -> str "type of impossible pattern-matching clause" - | MatchingVar _ -> str "matching variable" + | Evar_kinds.GoalEvar -> str "goal evar" + | Evar_kinds.ImpossibleCase -> str "type of impossible pattern-matching clause" + | Evar_kinds.MatchingVar _ -> str "matching variable" let pr_evar_info evi = let phyps = diff --git a/pretyping/evd.mli b/pretyping/evd.mli index bfdbf5e71..ca552a450 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -73,26 +73,6 @@ val map_clb : (constr -> constr) -> clbinding -> clbinding (******************************************************************** - ** Kinds of existential variables ***) - -(** Should the obligation be defined (opaque or transparent (default)) or - defined transparent and expanded in the term? *) - -type obligation_definition_status = Define of bool | Expand - -(** Evars *) -type hole_kind = - | ImplicitArg of global_reference * (int * identifier option) * bool (** Force inference *) - | BinderType of name - | QuestionMark of obligation_definition_status - | CasesType - | InternalHole - | TomatchTypeParameter of inductive * int - | GoalEvar - | ImpossibleCase - | MatchingVar of bool * identifier - -(******************************************************************** ** Existential variables and unification states ***) (** A unification state (of type [evar_map]) is primarily a finite mapping @@ -118,7 +98,7 @@ type evar_info = { evar_hyps : named_context_val; evar_body : evar_body; evar_filter : bool list; - evar_source : hole_kind located; + evar_source : Evar_kinds.t located; evar_candidates : constr list option; evar_extra : Store.t } @@ -199,9 +179,9 @@ val defined_evars : evar_map -> evar_map It optimizes the call of {!Evd.fold} to [f] and [undefined_evars m] *) val fold_undefined : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a val evar_declare : - named_context_val -> evar -> types -> ?src:loc * hole_kind -> + named_context_val -> evar -> types -> ?src:loc * Evar_kinds.t -> ?filter:bool list -> ?candidates:constr list -> evar_map -> evar_map -val evar_source : existential_key -> evar_map -> hole_kind located +val evar_source : existential_key -> evar_map -> Evar_kinds.t located (* spiwack: this function seems to somewhat break the abstraction. [evar_merge evd ev1] extends the evars of [evd] with [evd1] *) diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index 616a85444..fc1e1247f 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -15,7 +15,6 @@ open Sign open Term open Libnames open Nametab -open Evd (*i*) (* Untyped intermediate terms, after ASTs and before constr. *) @@ -67,7 +66,7 @@ type glob_constr = | GRec of loc * fix_kind * identifier array * glob_decl list array * glob_constr array * glob_constr array | GSort of loc * glob_sort - | GHole of (loc * hole_kind) + | GHole of (loc * Evar_kinds.t) | GCast of loc * glob_constr * glob_constr cast_type and glob_decl = name * binding_kind * glob_constr option * glob_constr diff --git a/pretyping/glob_term.mli b/pretyping/glob_term.mli index fca66fd28..d7d182833 100644 --- a/pretyping/glob_term.mli +++ b/pretyping/glob_term.mli @@ -70,7 +70,7 @@ type glob_constr = | GRec of loc * fix_kind * identifier array * glob_decl list array * glob_constr array * glob_constr array | GSort of loc * glob_sort - | GHole of (loc * Evd.hole_kind) + | GHole of (loc * Evar_kinds.t) | GCast of loc * glob_constr * glob_constr cast_type and glob_decl = name * binding_kind * glob_constr option * glob_constr diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 0610c00f1..47cc57fd1 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -111,7 +111,7 @@ let pattern_of_constr sigma t = match kind_of_term f with Evar (evk,args as ev) -> (match snd (Evd.evar_source evk sigma) with - MatchingVar (true,id) -> + Evar_kinds.MatchingVar (true,id) -> ctx := (id,None,existential_type sigma ev)::!ctx; Some id | _ -> None) @@ -124,10 +124,10 @@ let pattern_of_constr sigma t = | Construct sp -> PRef (canonical_gr (ConstructRef sp)) | Evar (evk,ctxt as ev) -> (match snd (Evd.evar_source evk sigma) with - | MatchingVar (b,id) -> + | Evar_kinds.MatchingVar (b,id) -> ctx := (id,None,existential_type sigma ev)::!ctx; assert (not b); PMeta (Some id) - | GoalEvar -> PEvar (evk,Array.map pattern_of_constr ctxt) + | Evar_kinds.GoalEvar -> PEvar (evk,Array.map pattern_of_constr ctxt) | _ -> PMeta None) | Case (ci,p,a,br) -> let cip = @@ -308,7 +308,8 @@ let rec pat_of_raw metas vars = function PIf (pat_of_raw metas vars c, pat_of_raw metas vars b1,pat_of_raw metas vars b2) | GLetTuple (loc,nal,(_,None),b,c) -> - let mkGLambda c na = GLambda (loc,na,Explicit,GHole (loc,Evd.InternalHole),c) in + let mkGLambda c na = + GLambda (loc,na,Explicit,GHole (loc,Evar_kinds.InternalHole),c) in let c = List.fold_left mkGLambda c nal in let cip = { cip_style = LetStyle; diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 409e405f5..e0cc2dec3 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -24,8 +24,8 @@ type pretype_error = | CantFindCaseType of constr (* Unification *) | OccurCheck of existential_key * constr - | NotClean of existential_key * constr * Evd.hole_kind - | UnsolvableImplicit of Evd.evar_info * Evd.hole_kind * + | NotClean of existential_key * constr * Evar_kinds.t + | UnsolvableImplicit of Evd.evar_info * Evar_kinds.t * Evd.unsolvability_explanation option | CannotUnify of constr * constr | CannotUnifyLocal of constr * constr * constr diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 43f934520..7debe2b0d 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -23,8 +23,8 @@ type pretype_error = | CantFindCaseType of constr (** Unification *) | OccurCheck of existential_key * constr - | NotClean of existential_key * constr * Evd.hole_kind - | UnsolvableImplicit of Evd.evar_info * Evd.hole_kind * + | NotClean of existential_key * constr * Evar_kinds.t + | UnsolvableImplicit of Evd.evar_info * Evar_kinds.t * Evd.unsolvability_explanation option | CannotUnify of constr * constr | CannotUnifyLocal of constr * constr * constr @@ -95,10 +95,10 @@ val error_cannot_coerce : env -> Evd.evar_map -> constr * constr -> 'b val error_occur_check : env -> Evd.evar_map -> existential_key -> constr -> 'b val error_not_clean : - env -> Evd.evar_map -> existential_key -> constr -> loc * Evd.hole_kind -> 'b + env -> Evd.evar_map -> existential_key -> constr -> loc * Evar_kinds.t -> 'b val error_unsolvable_implicit : - loc -> env -> Evd.evar_map -> Evd.evar_info -> Evd.hole_kind -> + loc -> env -> Evd.evar_map -> Evd.evar_info -> Evar_kinds.t -> Evd.unsolvability_explanation option -> 'b val error_cannot_unify : env -> Evd.evar_map -> constr * constr -> 'b diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 0205a52d5..d2553828f 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -245,7 +245,7 @@ let pretype_sort evdref = function exception Found of fixpoint let new_type_evar evdref env loc = - evd_comb0 (fun evd -> Evarutil.new_type_evar evd env ~src:(loc,InternalHole)) evdref + evd_comb0 (fun evd -> Evarutil.new_type_evar evd env ~src:(loc,Evar_kinds.InternalHole)) evdref (* [pretype tycon env evdref lvar lmeta cstr] attempts to type [cstr] *) (* in environment [env], with existential variables [evdref] and *) @@ -277,7 +277,7 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function match tycon with | Some ty -> ty | None -> new_type_evar evdref env loc in - let k = MatchingVar (someta,n) in + let k = Evar_kinds.MatchingVar (someta,n) in { uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty } | GHole (loc,k) -> diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index e6005391d..6be28ebcb 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -451,7 +451,7 @@ let is_instance = function is_class (IndRef ind) | _ -> false -let is_implicit_arg k = k <> GoalEvar +let is_implicit_arg k = k <> Evar_kinds.GoalEvar (* match k with *) (* ImplicitArg (ref, (n, id), b) -> true *) (* | InternalHole -> true *) diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index b1db243d6..7e283e56d 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -72,7 +72,7 @@ val instance_impl : instance -> global_reference val is_class : global_reference -> bool val is_instance : global_reference -> bool -val is_implicit_arg : hole_kind -> bool +val is_implicit_arg : Evar_kinds.t -> bool (** Returns the term and type for the given instance of the parameters and fields of the type class. *) diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index f6de344a9..6429116de 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -28,7 +28,7 @@ type typeclass_error = | NotAClass of constr | UnboundMethod of global_reference * identifier located (* Class name, method *) | NoInstance of identifier located * constr list - | UnsatisfiableConstraints of evar_map * (existential_key * hole_kind) option + | UnsatisfiableConstraints of evar_map * (existential_key * Evar_kinds.t) option | MismatchedContextInstance of contexts * constr_expr list * rel_context (* found, expected *) exception TypeClassError of env * typeclass_error diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli index fd709763d..3feb652ae 100644 --- a/pretyping/typeclasses_errors.mli +++ b/pretyping/typeclasses_errors.mli @@ -25,7 +25,7 @@ type typeclass_error = | NotAClass of constr | UnboundMethod of global_reference * identifier located (** Class name, method *) | NoInstance of identifier located * constr list - | UnsatisfiableConstraints of evar_map * (existential_key * hole_kind) option + | UnsatisfiableConstraints of evar_map * (existential_key * Evar_kinds.t) option | MismatchedContextInstance of contexts * constr_expr list * rel_context (** found, expected *) exception TypeClassError of env * typeclass_error diff --git a/pretyping/unification.ml b/pretyping/unification.ml index ce0af6853..2344f6e46 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -113,7 +113,7 @@ let pose_all_metas_as_evars env evd t = | None -> let {rebus=ty;freemetas=mvs} = Evd.meta_ftype evd mv in let ty = if mvs = Evd.Metaset.empty then ty else aux ty in - let ev = Evarutil.e_new_evar evdref env ~src:(dummy_loc,GoalEvar) ty in + let ev = Evarutil.e_new_evar evdref env ~src:(dummy_loc,Evar_kinds.GoalEvar) ty in evdref := meta_assign mv (ev,(Conv,TypeNotProcessed)) !evdref; ev) | _ -> @@ -774,7 +774,7 @@ let applyHead env evd n c = match kind_of_term (whd_betadeltaiota env evd cty) with | Prod (_,c1,c2) -> let (evd',evar) = - Evarutil.new_evar evd env ~src:(dummy_loc,GoalEvar) c1 in + Evarutil.new_evar evd env ~src:(dummy_loc,Evar_kinds.GoalEvar) c1 in apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd' | _ -> error "Apply_Head_Then" in diff --git a/proofs/clenv.ml b/proofs/clenv.ml index c4df5721f..cfe69c705 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -319,7 +319,7 @@ let clenv_pose_metas_as_evars clenv dep_mvs = if occur_meta ty then fold clenv (mvs@[mv]) else let (evd,evar) = - new_evar clenv.evd (cl_env clenv) ~src:(dummy_loc,GoalEvar) ty in + new_evar clenv.evd (cl_env clenv) ~src:(dummy_loc,Evar_kinds.GoalEvar) ty in let clenv = clenv_assign mv evar {clenv with evd=evd} in fold clenv mvs in fold clenv dep_mvs diff --git a/proofs/goal.ml b/proofs/goal.ml index 37bb96de7..cef43c443 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -498,7 +498,7 @@ module V82 = struct Evd.evar_filter = List.map (fun _ -> true) (Environ.named_context_of_val hyps); Evd.evar_body = Evd.Evar_empty; - Evd.evar_source = (Pp.dummy_loc,Evd.GoalEvar); + Evd.evar_source = (Pp.dummy_loc,Evar_kinds.GoalEvar); Evd.evar_candidates = None; Evd.evar_extra = extra } in diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 320e01f4f..2f3f58dc3 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -179,7 +179,7 @@ let declare_implicit_tactic tac = implicit_tactic := Some tac let solve_by_implicit_tactic env sigma (evk,args) = let evi = Evd.find_undefined sigma evk in match (!implicit_tactic, snd (evar_source evk sigma)) with - | Some tac, (ImplicitArg _ | QuestionMark _) + | Some tac, (Evar_kinds.ImplicitArg _ | Evar_kinds.QuestionMark _) when Sign.named_context_equal (Environ.named_context_of_val evi.evar_hyps) (Environ.named_context env) -> diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 24c3a5d9f..f4c032e73 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -585,8 +585,8 @@ let is_inference_forced p evd ev = then let (loc, k) = evar_source ev evd in match k with - | ImplicitArg (_, _, b) -> b - | QuestionMark _ -> false + | Evar_kinds.ImplicitArg (_, _, b) -> b + | Evar_kinds.QuestionMark _ -> false | _ -> true else true with Not_found -> assert false @@ -683,7 +683,7 @@ let initial_select_evars with_goals = Typeclasses.is_class_evar evd evi) else (fun evd ev evi -> - (snd (Evd.evar_source ev evd) <> Evd.GoalEvar) + (snd (Evd.evar_source ev evd) <> Evar_kinds.GoalEvar) && Typeclasses.is_class_evar evd evi) let resolve_typeclass_evars debug m env evd with_goals split fail = diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index f1341762a..a33b6b19b 100644 --- a/tactics/evar_tactics.ml +++ b/tactics/evar_tactics.ml @@ -52,7 +52,7 @@ let instantiate n (ist,rawc) ido gl = gl let let_evar name typ gls = - let src = (dummy_loc,GoalEvar) in + let src = (dummy_loc,Evar_kinds.GoalEvar) in let sigma',evar = Evarutil.new_evar gls.sigma (pf_env gls) ~src typ in Refiner.tclTHEN (Refiner.tclEVARS sigma') (Tactics.letin_tac None name evar None nowhere) gls diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 61ffe599f..e497581ed 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -558,8 +558,13 @@ let subst_var_with_hole occ tid t = let rec substrec = function | GVar (_,id) as x -> if id = tid - then (decr occref; if !occref = 0 then x - else (incr locref; GHole (make_loc (!locref,0),Evd.QuestionMark(Evd.Define true)))) + then + (decr occref; + if !occref = 0 then x + else + (incr locref; + GHole (make_loc (!locref,0), + Evar_kinds.QuestionMark(Evar_kinds.Define true)))) else x | c -> map_glob_constr_left_to_right substrec c in let t' = substrec t @@ -570,9 +575,13 @@ let subst_hole_with_term occ tc t = let locref = ref 0 in let occref = ref occ in let rec substrec = function - | GHole (_,Evd.QuestionMark(Evd.Define true)) -> - decr occref; if !occref = 0 then tc - else (incr locref; GHole (make_loc (!locref,0),Evd.QuestionMark(Evd.Define true))) + | GHole (_,Evar_kinds.QuestionMark(Evar_kinds.Define true)) -> + decr occref; + if !occref = 0 then tc + else + (incr locref; + GHole (make_loc (!locref,0), + Evar_kinds.QuestionMark(Evar_kinds.Define true))) | c -> map_glob_constr_left_to_right substrec c in substrec t diff --git a/toplevel/classes.ml b/toplevel/classes.ml index dbabf6160..b3b9efcef 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -231,7 +231,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props k.cl_projs; c :: props, rest' with Not_found -> - (CHole (Pp.dummy_loc, Some Evd.GoalEvar) :: props), rest + (CHole (Pp.dummy_loc, Some Evar_kinds.GoalEvar) :: props), rest else props, rest) ([], props) k.cl_props in diff --git a/toplevel/command.ml b/toplevel/command.ml index 5aef9ec66..9e21a3a76 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -683,7 +683,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation = mkApp (constr_of_global (delayed_force fix_sub_ref), [| argtyp ; wf_rel ; Evarutil.e_new_evar isevars env - ~src:(dummy_loc, Evd.QuestionMark (Evd.Define false)) wf_proof; + ~src:(dummy_loc, Evar_kinds.QuestionMark (Evar_kinds.Define false)) wf_proof; prop ; intern_body_lam |]) in let _ = isevars := Evarutil.nf_evar_map !isevars in @@ -866,8 +866,8 @@ let check_program_evars env initial_sigma evd c = if not (Evd.mem initial_sigma evk) then let (loc,k) = Evd.evar_source evk evd in (match k with - | Evd.QuestionMark _ - | Evd.ImplicitArg (_, _, false) -> () + | Evar_kinds.QuestionMark _ + | Evar_kinds.ImplicitArg (_, _, false) -> () | _ -> let evi = nf_evar_info sigma (Evd.find sigma evk) in Pretype_errors.error_unsolvable_implicit loc env sigma evi k None) diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 051eb3062..e0923cda0 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -342,35 +342,35 @@ let pr_ne_context_of header footer env = then footer else pr_ne_context_of header env -let explain_hole_kind env evi = function - | QuestionMark _ -> str "this placeholder" - | CasesType -> +let explain_evar_kind env evi = function + | Evar_kinds.QuestionMark _ -> str "this placeholder" + | Evar_kinds.CasesType -> str "the type of this pattern-matching problem" - | BinderType (Name id) -> + | Evar_kinds.BinderType (Name id) -> str "the type of " ++ Nameops.pr_id id - | BinderType Anonymous -> + | Evar_kinds.BinderType Anonymous -> str "the type of this anonymous binder" - | ImplicitArg (c,(n,ido),b) -> + | Evar_kinds.ImplicitArg (c,(n,ido),b) -> let id = Option.get ido in str "the implicit parameter " ++ pr_id id ++ spc () ++ str "of" ++ spc () ++ Nametab.pr_global_env Idset.empty c - | InternalHole -> + | Evar_kinds.InternalHole -> str "an internal placeholder" ++ Option.cata (fun evi -> let env = Evd.evar_env evi in str " of type " ++ pr_lconstr_env env evi.evar_concl ++ pr_ne_context_of (str " in environment:"++ fnl ()) (mt ()) env) (mt ()) evi - | TomatchTypeParameter (tyi,n) -> + | Evar_kinds.TomatchTypeParameter (tyi,n) -> str "the " ++ pr_nth n ++ str " argument of the inductive type (" ++ pr_inductive env tyi ++ str ") of this term" - | GoalEvar -> + | Evar_kinds.GoalEvar -> str "an existential variable" - | ImpossibleCase -> + | Evar_kinds.ImpossibleCase -> str "the type of an impossible pattern-matching clause" - | MatchingVar _ -> + | Evar_kinds.MatchingVar _ -> assert false let explain_not_clean env sigma ev t k = @@ -378,7 +378,7 @@ let explain_not_clean env sigma ev t k = let env = make_all_name_different env in let id = Evd.string_of_existential ev in let var = pr_lconstr_env env t in - str "Tried to instantiate " ++ explain_hole_kind env None k ++ + str "Tried to instantiate " ++ explain_evar_kind env None k ++ str " (" ++ str id ++ str ")" ++ spc () ++ str "with a term using variable " ++ var ++ spc () ++ str "which is not in its scope." @@ -398,7 +398,7 @@ let explain_typeclass_resolution env evi k = | None -> mt() let explain_unsolvable_implicit env evi k explain = - str "Cannot infer " ++ explain_hole_kind env (Some evi) k ++ + str "Cannot infer " ++ explain_evar_kind env (Some evi) k ++ explain_unsolvability explain ++ str "." ++ explain_typeclass_resolution env evi k @@ -693,7 +693,7 @@ let explain_no_instance env (_,id) l = str "applied to arguments" ++ spc () ++ pr_sequence (pr_lconstr_env env) l -let is_goal_evar evi = match evi.evar_source with (_, GoalEvar) -> true | _ -> false +let is_goal_evar evi = match evi.evar_source with (_, Evar_kinds.GoalEvar) -> true | _ -> false let pr_constraints printenv env evm = let evm = Evd.undefined_evars (Evarutil.nf_evar_map_undefined evm) in diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 589403882..c6bb2c10a 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -49,8 +49,8 @@ let check_evars env evm = (fun (key, evi) -> let (loc,k) = evar_source key evm in match k with - | QuestionMark _ - | ImplicitArg (_,_,false) -> () + | Evar_kinds.QuestionMark _ + | Evar_kinds.ImplicitArg (_,_,false) -> () | _ -> Pretype_errors.error_unsolvable_implicit loc env evm (Evarutil.nf_evar_info evm evi) k None) @@ -59,9 +59,9 @@ let check_evars env evm = type oblinfo = { ev_name: int * identifier; ev_hyps: named_context; - ev_status: obligation_definition_status; + ev_status: Evar_kinds.obligation_definition_status; ev_chop: int option; - ev_src: hole_kind located; + ev_src: Evar_kinds.t located; ev_typ: types; ev_tac: tactic option; ev_deps: Intset.t } @@ -252,13 +252,13 @@ let eterm_obligations env name evm fs ?status t ty = | None -> evtyp, hyps, 0 in let loc, k = evar_source id evm in - let status = match k with QuestionMark o -> Some o | _ -> status in + let status = match k with Evar_kinds.QuestionMark o -> Some o | _ -> status in let status, chop = match status with - | Some (Define true as stat) -> - if chop <> fs then Define false, None + | Some (Evar_kinds.Define true as stat) -> + if chop <> fs then Evar_kinds.Define false, None else stat, Some chop | Some s -> s, None - | None -> Define true, None + | None -> Evar_kinds.Define true, None in let tac = match evar_tactic.get ev.evar_extra with | Some t -> @@ -284,7 +284,8 @@ let eterm_obligations env name evm fs ?status t ty = ev_src = src; ev_typ = typ; ev_deps = deps; ev_tac = tac } = info in let status = match status with - | Define true when Idset.mem name transparent -> Define false + | Evar_kinds.Define true when Idset.mem name transparent -> + Evar_kinds.Define false | _ -> status in name, typ, src, status, deps, tac) evts in @@ -312,15 +313,16 @@ let explain_no_obligations = function Some ident -> str "No obligations for program " ++ str (string_of_id ident) | None -> str "No obligations remaining" -type obligation_info = (Names.identifier * Term.types * hole_kind located * - obligation_definition_status * Intset.t * tactic option) array +type obligation_info = + (Names.identifier * Term.types * Evar_kinds.t located * + Evar_kinds.obligation_definition_status * Intset.t * tactic option) array type obligation = { obl_name : identifier; obl_type : types; - obl_location : hole_kind located; + obl_location : Evar_kinds.t located; obl_body : constr option; - obl_status : obligation_definition_status; + obl_status : Evar_kinds.obligation_definition_status; obl_deps : Intset.t; obl_tac : tactic option; } @@ -391,7 +393,7 @@ let evar_of_obligation o = make_evar (Global.named_context_val ()) o.obl_type let get_obligation_body expand obl = let c = Option.get obl.obl_body in - if expand && obl.obl_status = Expand then + if expand && obl.obl_status = Evar_kinds.Expand then match kind_of_term c with | Const c -> constant_value (Global.env ()) c | _ -> c @@ -603,8 +605,8 @@ let declare_obligation prg obl body = let body = prg.prg_reduce body in let ty = prg.prg_reduce obl.obl_type in match obl.obl_status with - | Expand -> { obl with obl_body = Some body } - | Define opaque -> + | Evar_kinds.Expand -> { obl with obl_body = Some body } + | Evar_kinds.Define opaque -> let opaque = if get_proofs_transparency () then false else opaque in let ce = { const_entry_body = body; @@ -628,8 +630,9 @@ let init_prog_info n b t deps fixkind notations obls impls kind reduce hook = assert(obls = [||]); let n = Nameops.add_suffix n "_obligation" in [| { obl_name = n; obl_body = None; - obl_location = dummy_loc, InternalHole; obl_type = t; - obl_status = Expand; obl_deps = Intset.empty; obl_tac = None } |], + obl_location = dummy_loc, Evar_kinds.InternalHole; obl_type = t; + obl_status = Evar_kinds.Expand; obl_deps = Intset.empty; + obl_tac = None } |], mkVar n | Some b -> Array.mapi @@ -726,7 +729,7 @@ let goal_fix_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Fixp let kind_of_opacity o = match o with - | Define false | Expand -> goal_kind + | Evar_kinds.Define false | Evar_kinds.Expand -> goal_kind | _ -> goal_proof_kind let not_transp_msg = @@ -774,10 +777,10 @@ let rec solve_obligation prg num tac = let transparent = evaluable_constant cst (Global.env ()) in let body = match obl.obl_status with - | Expand -> + | Evar_kinds.Expand -> if not transparent then error_not_transp () else constant_value (Global.env ()) cst - | Define opaque -> + | Evar_kinds.Define opaque -> if not opaque && not transparent then error_not_transp () else Libnames.constr_of_global gr in diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli index 16c00ce8f..df093ea43 100644 --- a/toplevel/obligations.mli +++ b/toplevel/obligations.mli @@ -39,8 +39,8 @@ val sort_dependencies : (int * evar_info * Intset.t) list -> (int * evar_info * (* env, id, evars, number of function prototypes to try to clear from evars contexts, object and type *) val eterm_obligations : env -> identifier -> evar_map -> int -> - ?status:obligation_definition_status -> constr -> types -> - (identifier * types * hole_kind located * obligation_definition_status * Intset.t * + ?status:Evar_kinds.obligation_definition_status -> constr -> types -> + (identifier * types * Evar_kinds.t located * Evar_kinds.obligation_definition_status * Intset.t * tactic option) array (* Existential key, obl. name, type as product, location of the original evar, associated tactic, @@ -52,8 +52,8 @@ val eterm_obligations : env -> identifier -> evar_map -> int -> translation from obligation identifiers to constrs, new term, new type *) type obligation_info = - (identifier * Term.types * hole_kind located * - obligation_definition_status * Intset.t * tactic option) array + (identifier * Term.types * Evar_kinds.t located * + Evar_kinds.obligation_definition_status * Intset.t * tactic option) array (* ident, type, location, (opaque or transparent, expand or define), dependencies, tactic to solve it *) |