From 538b77dbb3b7799dc4d2e18033fc4fbf2eb26f7f Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 30 Sep 2014 09:13:40 +0200 Subject: Add syntax for naming new goals in refine: writing ?[id] instead of _ will name the goal id; writing ?[?id] will use the first fresh name available based with prefix id. Tactics intro, rename, change, ... from logic.ml now preserve goal name; cut preserves goal name on its main premise. --- grammar/q_constr.ml4 | 2 +- grammar/q_coqast.ml4 | 6 ++--- interp/constrexpr_ops.ml | 4 +-- interp/constrextern.ml | 10 +++---- interp/constrintern.ml | 42 +++++++++++++++--------------- interp/notation.ml | 2 +- interp/notation_ops.ml | 18 ++++++------- interp/topconstr.ml | 2 +- intf/constrexpr.mli | 2 +- intf/glob_term.mli | 2 +- intf/notation_term.mli | 2 +- parsing/egramcoq.ml | 2 +- parsing/g_constr.ml4 | 49 +++++++++++++++++++---------------- parsing/g_ltac.ml4 | 2 +- parsing/g_tactic.ml4 | 2 +- parsing/g_vernac.ml4 | 6 ++--- plugins/decl_mode/decl_interp.ml | 12 ++++----- plugins/decl_mode/decl_proof_instr.ml | 2 +- plugins/firstorder/instances.ml | 2 +- plugins/funind/glob_termops.ml | 2 +- plugins/syntax/numbers_syntax.ml | 4 +-- pretyping/cases.ml | 2 +- pretyping/detyping.ml | 4 +-- pretyping/evarutil.ml | 24 ++++++++--------- pretyping/evarutil.mli | 18 ++++++++----- pretyping/evd.ml | 43 ++++++++++++++++++++++-------- pretyping/evd.mli | 6 +++-- pretyping/glob_ops.ml | 9 ++++--- pretyping/miscops.ml | 7 +++++ pretyping/miscops.mli | 5 ++++ pretyping/patternops.ml | 2 +- pretyping/pretyping.ml | 10 +++---- printing/ppconstr.ml | 16 +++++++----- printing/ppvernac.ml | 2 +- proofs/goal.ml | 7 ++++- proofs/goal.mli | 7 +++-- proofs/logic.ml | 16 ++++++------ stm/texmacspp.ml | 2 +- tactics/extratactics.ml4 | 7 ++--- tactics/rewrite.ml | 2 +- toplevel/classes.ml | 4 +-- toplevel/command.ml | 2 +- toplevel/record.ml | 2 +- 43 files changed, 216 insertions(+), 156 deletions(-) diff --git a/grammar/q_constr.ml4 b/grammar/q_constr.ml4 index e1db0a05a..bd3fac2e7 100644 --- a/grammar/q_constr.ml4 +++ b/grammar/q_constr.ml4 @@ -70,7 +70,7 @@ EXTEND | "0" [ s = sort -> <:expr< Glob_term.GSort ($dloc$,s) >> | id = ident -> <:expr< Glob_term.GVar ($dloc$,$id$) >> - | "_" -> <:expr< Glob_term.GHole ($dloc$,Evar_kinds.QuestionMark (Evar_kinds.Define False),None) >> + | "_" -> <:expr< Glob_term.GHole ($dloc$,Evar_kinds.QuestionMark (Evar_kinds.Define False),Misctypes.IntroAnonymous,None) >> | "?"; id = ident -> <:expr< Glob_term.GPatVar($dloc$,(False,$id$)) >> | "{"; c1 = constr; "}"; "+"; "{"; c2 = constr; "}" -> apply_ref <:expr< coq_sumbool_ref >> [c1;c2] diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4 index f59a4af32..25d4c0b23 100644 --- a/grammar/q_coqast.ml4 +++ b/grammar/q_coqast.ml4 @@ -166,10 +166,10 @@ let rec mlexpr_of_constr = function let loc = of_coqloc loc in <:expr< Constrexpr.CApp $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_constr a$ $mlexpr_of_list (mlexpr_of_pair mlexpr_of_constr (mlexpr_of_option (mlexpr_of_located mlexpr_of_explicitation))) l$ >> | Constrexpr.CCases (loc,_,_,_,_) -> failwith "mlexpr_of_constr: TODO" - | Constrexpr.CHole (loc, None, None) -> + | Constrexpr.CHole (loc, None, ipat, None) -> let loc = of_coqloc loc in - <:expr< Constrexpr.CHole $dloc$ None None >> - | Constrexpr.CHole (loc, _, _) -> failwith "mlexpr_of_constr: TODO CHole (Some _)" + <:expr< Constrexpr.CHole $dloc$ None $mlexpr_of_intro_pattern_naming ipat$ None >> + | Constrexpr.CHole (loc,_,_,_) -> failwith "mlexpr_of_constr: TODO CHole (Some _)" | Constrexpr.CNotation(_,ntn,(subst,substl,[])) -> <:expr< Constrexpr.CNotation $dloc$ $mlexpr_of_string ntn$ ($mlexpr_of_list mlexpr_of_constr subst$, diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 01efef940..6056c9b9d 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -242,7 +242,7 @@ let constr_loc = function | CCases (loc,_,_,_,_) -> loc | CLetTuple (loc,_,_,_,_) -> loc | CIf (loc,_,_,_,_) -> loc - | CHole (loc, _, _) -> loc + | CHole (loc,_,_,_) -> loc | CPatVar (loc,_) -> loc | CEvar (loc,_,_) -> loc | CSort (loc,_) -> loc @@ -339,7 +339,7 @@ let coerce_to_id = function let coerce_to_name = function | CRef (Ident (loc,id),_) -> (loc,Name id) - | CHole (loc,_,_) -> (loc,Anonymous) + | CHole (loc,_,_,_) -> (loc,Anonymous) | a -> Errors.user_err_loc (constr_loc a,"coerce_to_name", str "This expression should be a name.") diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 63461c11a..8e6485b7b 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -629,13 +629,13 @@ let rec extern inctx scopes vars r = | GVar (loc,id) -> CRef (Ident (loc,id),None) - | GEvar (loc,n,[]) when !print_meta_as_hole -> CHole (loc, None, None) + | GEvar (loc,n,[]) when !print_meta_as_hole -> CHole (loc, None, Misctypes.IntroAnonymous, None) | GEvar (loc,n,l) -> extern_evar loc n (List.map (on_snd (extern false scopes vars)) l) | GPatVar (loc,(b,n)) -> - if !print_meta_as_hole then CHole (loc, None, None) else + if !print_meta_as_hole then CHole (loc, None, Misctypes.IntroAnonymous, None) else if b then CPatVar (loc,n) else CEvar (loc,n,[]) | GApp (loc,f,args) -> @@ -782,7 +782,7 @@ let rec extern inctx scopes vars r = | GSort (loc,s) -> CSort (loc,extern_glob_sort s) - | GHole (loc,e,_) -> CHole (loc, Some e, None) (** TODO: extern tactics. *) + | GHole (loc,e,naming,_) -> CHole (loc, Some e, naming, None) (** TODO: extern tactics. *) | GCast (loc,c, c') -> CCast (loc,sub_extern true scopes vars c, @@ -964,7 +964,7 @@ let extern_sort s = extern_glob_sort (detype_sort s) let any_any_branch = (* | _ => _ *) - (loc,[],[PatVar (loc,Anonymous)],GHole (loc,Evar_kinds.InternalHole,None)) + (loc,[],[PatVar (loc,Anonymous)],GHole (loc,Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None)) let rec glob_of_pat env sigma = function | PRef ref -> GRef (loc,ref,None) @@ -981,7 +981,7 @@ let rec glob_of_pat env sigma = function anomaly ~label:"glob_constr_of_pattern" (Pp.str "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,Evar_kinds.InternalHole, None) + | PMeta None -> GHole (loc,Evar_kinds.InternalHole, Misctypes.IntroAnonymous,None) | PMeta (Some n) -> GPatVar (loc,(false,n)) | PProj (p,c) -> GApp (loc,GRef (loc, ConstRef (Projection.constant p),None), [glob_of_pat env sigma c]) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 6b3de2621..a0654220e 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -345,13 +345,13 @@ let rec check_capture ty = function | [] -> () -let locate_if_isevar loc na = function - | GHole _ -> +let locate_if_hole loc na = function + | GHole (_,_,naming,arg) -> (try match na with | Name id -> glob_constr_of_notation_constr loc (Reserve.find_reserved_type id) | Anonymous -> raise Not_found - with Not_found -> GHole (loc, Evar_kinds.BinderType na, None)) + with Not_found -> GHole (loc, Evar_kinds.BinderType na, naming, arg)) | x -> x let reset_hidden_inductive_implicit_test env = @@ -398,7 +398,7 @@ let intern_generalized_binder ?(global_level=false) intern_type lvar env fvs in let bl = List.map (fun (id, loc) -> - (loc, (Name id, b, None, GHole (loc, Evar_kinds.BinderType (Name id), None)))) + (loc, (Name id, b, None, GHole (loc, Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None)))) fvs in let na = match na with @@ -425,7 +425,7 @@ let intern_assumption intern lvar env nal bk ty = List.fold_left (fun (env, bl) (loc, na as locna) -> (push_name_env lvar impls env locna, - (loc,(na,k,None,locate_if_isevar loc na ty))::bl)) + (loc,(na,k,None,locate_if_hole loc na ty))::bl)) (env, []) nal | Generalized (b,b',t) -> let env, b = intern_generalized_binder intern_type lvar env (List.hd nal) b b' t ty in @@ -438,7 +438,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,Evar_kinds.BinderType na,None)))::bl) + (loc,(na,Explicit,Some(indef),GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None)))::bl) let intern_generalization intern env lvar loc bk ak c = let c = intern {env with unb = true} c in @@ -458,10 +458,10 @@ let intern_generalization intern env lvar loc bk ak c = in if pi then (fun (id, loc') acc -> - GProd (Loc.merge loc' loc, Name id, bk, GHole (loc', Evar_kinds.BinderType (Name id), None), acc)) + GProd (Loc.merge loc' loc, Name id, bk, GHole (loc', Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc)) else (fun (id, loc') acc -> - GLambda (Loc.merge loc' loc, Name id, bk, GHole (loc', Evar_kinds.BinderType (Name id), None), acc)) + GLambda (Loc.merge loc' loc, Name id, bk, GHole (loc', Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc)) in List.fold_right (fun (id, loc as lid) (env, acc) -> let env' = push_name_env lvar (Variable,[],[],[]) env (loc, Name id) in @@ -541,7 +541,7 @@ let subst_aconstr_in_glob_constr loc intern lvar subst infos c = List.fold_right fold (if lassoc then List.rev l else l) termin with Not_found -> anomaly (Pp.str "Inconsistent substitution of recursive notation")) - | NHole (knd, arg) -> + | NHole (knd, naming, arg) -> let knd = match knd with | Evar_kinds.BinderType (Name id as na) -> let na = @@ -572,7 +572,7 @@ let subst_aconstr_in_glob_constr loc intern lvar subst infos c = let arg = in_gen wit tac in Some arg in - GHole (loc, knd, arg) + GHole (loc, knd, naming, arg) | NBinderList (x,_,iter,terminator) -> (try (* All elements of the list are in scopes (scopt,subscopes) *) @@ -1299,8 +1299,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,Evar_kinds.ImplicitArg (r,i,b),None) - | GVar (loc,id) -> (loc,Evar_kinds.ImplicitArg (VarRef id,i,b),None) + | GRef (loc,r,_) | GApp (_,GRef (loc,r,_),_) -> (loc,Evar_kinds.ImplicitArg (r,i,b),Misctypes.IntroAnonymous,None) + | GVar (loc,id) -> (loc,Evar_kinds.ImplicitArg (VarRef id,i,b),Misctypes.IntroAnonymous,None) | _ -> anomaly (Pp.str "Only refs have implicits") let exists_implicit_name id = @@ -1476,13 +1476,13 @@ let internalize globalenv env allow_patvar lvar c = | CRecord (loc, _, fs) -> let cargs = sort_fields true loc fs - (fun k l -> CHole (loc, Some (Evar_kinds.QuestionMark (Evar_kinds.Define true)), None) :: l) + (fun k l -> CHole (loc, Some (Evar_kinds.QuestionMark (Evar_kinds.Define true)), Misctypes.IntroAnonymous, None) :: l) in begin match cargs with | None -> user_err_loc (loc, "intern", str"No constructor inference.") | Some (n, constrname, args) -> - let pars = List.make n (CHole (loc, None, None)) in + let pars = List.make n (CHole (loc, None, Misctypes.IntroAnonymous, None)) in let app = CAppExpl (loc, (None, constrname,None), List.rev_append pars args) in intern env app end @@ -1514,9 +1514,9 @@ let internalize globalenv env allow_patvar lvar c = GCases(Loc.ghost,Term.RegularStyle,(* Some (GSort (Loc.ghost,GType None)) *)None, (* "return Type" *) List.map (fun id -> GVar (Loc.ghost,id),(Name id,None)) thevars, (* "match v1,..,vn" *) [Loc.ghost,[],thepats, (* "|p1,..,pn" *) - Option.cata (intern_type env') (GHole(Loc.ghost,Evar_kinds.CasesType,None)) rtnpo; (* "=> P" is there were a P "=> _" else *) + Option.cata (intern_type env') (GHole(Loc.ghost,Evar_kinds.CasesType,Misctypes.IntroAnonymous,None)) rtnpo; (* "=> P" is there were a P "=> _" else *) Loc.ghost,[],List.make (List.length thepats) (PatVar(Loc.ghost,Anonymous)), (* "|_,..,_" *) - GHole(Loc.ghost,Evar_kinds.ImpossibleCase,None) (* "=> _" *)])) + GHole(Loc.ghost,Evar_kinds.ImpossibleCase,Misctypes.IntroAnonymous,None) (* "=> _" *)])) in let eqns' = List.map (intern_eqn (List.length tms) env) eqns in GCases (loc, sty, rtnpo, tms, List.flatten eqns') @@ -1538,7 +1538,7 @@ let internalize globalenv env allow_patvar lvar c = (Loc.ghost,na') in intern_type env'' p) po in GIf (loc, c', (na', p'), intern env b1, intern env b2) - | CHole (loc, k, solve) -> + | CHole (loc, k, naming, solve) -> let k = match k with | None -> Evar_kinds.QuestionMark (Evar_kinds.Define true) | Some k -> k @@ -1559,7 +1559,7 @@ let internalize globalenv env allow_patvar lvar c = let (_, glb) = Genintern.generic_intern ist gen in Some glb in - GHole (loc, k, solve) + GHole (loc, k, naming, solve) (* Parsing pattern variables *) | CPatVar (loc, n) when allow_patvar -> GPatVar (loc, (true,n)) @@ -1856,12 +1856,12 @@ let interp_notation_constr ?(impls=empty_internalization_env) nenv a = let interp_binder env sigma na t = let t = intern_gen IsType env t in - let t' = locate_if_isevar (loc_of_glob_constr t) na t in + let t' = locate_if_hole (loc_of_glob_constr t) na t in understand ~expected_type:IsType env sigma t' let interp_binder_evars env evdref na t = let t = intern_gen IsType env t in - let t' = locate_if_isevar (loc_of_glob_constr t) na t in + let t' = locate_if_hole (loc_of_glob_constr t) na t in understand_tcc_evars env evdref ~expected_type:IsType t' open Environ @@ -1886,7 +1886,7 @@ let interp_rawcontext_evars env evdref bl = (fun (env,params,n,impls) (na, k, b, t) -> match b with None -> - let t' = locate_if_isevar (loc_of_glob_constr t) na t in + let t' = locate_if_hole (loc_of_glob_constr t) na t in let t = understand_tcc_evars env evdref ~expected_type:IsType t' in let d = (na,None,t) in diff --git a/interp/notation.ml b/interp/notation.ml index 93e6f31c0..de7eca352 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -442,7 +442,7 @@ let interp_prim_token = let rec rcp_of_glob looked_for = function | GVar (loc,id) -> RCPatAtom (loc,Some id) - | GHole (loc,_,_) -> RCPatAtom (loc,None) + | GHole (loc,_,_,_) -> RCPatAtom (loc,None) | GRef (loc,g,_) -> looked_for g; RCPatCstr (loc, g,[],[]) | GApp (loc,GRef (_,g,_),l) -> looked_for g; RCPatCstr (loc, g, List.map (rcp_of_glob looked_for) l,[]) diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 81e2ac810..f4b74d62c 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -104,7 +104,7 @@ let glob_constr_of_notation_constr_with_binders loc g f e = function GRec (loc,fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl) | NCast (c,k) -> GCast (loc,f e c,Miscops.map_cast_type (f e) k) | NSort x -> GSort (loc,x) - | NHole (x, arg) -> GHole (loc, x, arg) + | NHole (x, naming, arg) -> GHole (loc, x, naming, arg) | NPatVar n -> GPatVar (loc,(false,n)) | NRef x -> GRef (loc,x,None) @@ -287,7 +287,7 @@ let notation_constr_and_vars_of_glob_constr a = NRec (fk,idl,dll,Array.map aux tl,Array.map aux bl) | GCast (_,c,k) -> NCast (aux c,Miscops.map_cast_type aux k) | GSort (_,s) -> NSort s - | GHole (_,w,arg) -> NHole (w, arg) + | GHole (_,w,naming,arg) -> NHole (w, naming, arg) | GRef (_,r,_) -> NRef r | GPatVar (_,(_,n)) -> NPatVar n | GEvar _ -> @@ -465,7 +465,7 @@ let rec subst_notation_constr subst bound raw = | NPatVar _ | NSort _ -> raw - | NHole (knd, solve) -> + | NHole (knd, naming, solve) -> let nknd = match knd with | Evar_kinds.ImplicitArg (ref, i, b) -> let nref, _ = subst_global subst ref in @@ -474,7 +474,7 @@ let rec subst_notation_constr subst bound raw = in let nsolve = Option.smartmap (Genintern.generic_substitute subst) solve in if nsolve == solve && nknd == knd then raw - else NHole (nknd, nsolve) + else NHole (nknd, naming, nsolve) | NCast (r1,k) -> let r1' = subst_notation_constr subst bound r1 in @@ -498,11 +498,11 @@ 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(Loc.ghost,na,Explicit,GHole(Loc.ghost,Evar_kinds.InternalHole,None),c)) + GLambda(Loc.ghost,na,Explicit,GHole(Loc.ghost,Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None),c)) let abstract_return_type_context_notation_constr = abstract_return_type_context snd - (fun na c -> NLambda(na,NHole (Evar_kinds.InternalHole, None),c)) + (fun na c -> NLambda(na,NHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None),c)) exception No_match @@ -555,7 +555,7 @@ let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with | (_,Name id2) when Id.List.mem id2 (fst metas) -> let rhs = match na1 with | Name id1 -> GVar (Loc.ghost,id1) - | Anonymous -> GHole (Loc.ghost,Evar_kinds.InternalHole,None) in + | Anonymous -> GHole (Loc.ghost,Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None) in alp, bind_env alp sigma id2 rhs | (Name id1,Name id2) -> (id1,id2)::alp,sigma | (Anonymous,Anonymous) -> alp,sigma @@ -579,7 +579,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,Evar_kinds.BinderType na,None))::decls) b + ((na,Explicit (*?*), Some c,GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None))::decls) b | b -> (decls,b) let remove_sigma x (sigmavar,sigmalist,sigmabinders) = @@ -733,7 +733,7 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 = to print "{x:_ & P x}" knowing that notation "{x & P x}" is not defined. *) | b1, NLambda (Name id,(NHole _ | NVar _ as t2),b2) when inner -> let id' = Namegen.next_ident_away id (free_glob_vars b1) in - let t1 = GHole(Loc.ghost,Evar_kinds.BinderType (Name id'),None) in + let t1 = GHole(Loc.ghost,Evar_kinds.BinderType (Name id'),Misctypes.IntroAnonymous,None) in let sigma = match t2 with | NHole _ -> sigma | NVar id2 -> bind_env alp sigma id2 t1 diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 97f9429c1..62b268b48 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -111,7 +111,7 @@ let fold_constr_expr_with_binders g f n acc = function (* The following is an approximation: we don't know exactly if an ident is binding nor to which subterms bindings apply *) let acc = List.fold_left (f n) acc (l@List.flatten ll) in - List.fold_left (fun acc bl -> fold_local_binders g f n acc (CHole (Loc.ghost,None,None)) bl) acc bll + List.fold_left (fun acc bl -> fold_local_binders g f n acc (CHole (Loc.ghost,None,IntroAnonymous,None)) bl) acc bll | CGeneralization (_,_,_,c) -> f n acc c | CDelimiters (loc,_,a) -> f n acc a | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CRef _ -> diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index f6660ff69..6b17e0286 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -80,7 +80,7 @@ type constr_expr = constr_expr * constr_expr | CIf of Loc.t * constr_expr * (Name.t located option * constr_expr option) * constr_expr * constr_expr - | CHole of Loc.t * Evar_kinds.t option * Genarg.raw_generic_argument option + | CHole of Loc.t * Evar_kinds.t option * intro_pattern_naming_expr * Genarg.raw_generic_argument option | CPatVar of Loc.t * patvar | CEvar of Loc.t * Glob_term.existential_name * (Id.t * constr_expr) list | CSort of Loc.t * glob_sort diff --git a/intf/glob_term.mli b/intf/glob_term.mli index 832ee4e4b..2a48f3432 100644 --- a/intf/glob_term.mli +++ b/intf/glob_term.mli @@ -47,7 +47,7 @@ type glob_constr = | GRec of Loc.t * fix_kind * Id.t array * glob_decl list array * glob_constr array * glob_constr array | GSort of Loc.t * glob_sort - | GHole of (Loc.t * Evar_kinds.t * Genarg.glob_generic_argument option) + | GHole of (Loc.t * Evar_kinds.t * intro_pattern_naming_expr * Genarg.glob_generic_argument option) | GCast of Loc.t * glob_constr * glob_constr cast_type and glob_decl = Name.t * binding_kind * glob_constr option * glob_constr diff --git a/intf/notation_term.mli b/intf/notation_term.mli index daf605ab2..5d9c1c177 100644 --- a/intf/notation_term.mli +++ b/intf/notation_term.mli @@ -24,7 +24,7 @@ type notation_constr = | NRef of global_reference | NVar of Id.t | NApp of notation_constr * notation_constr list - | NHole of Evar_kinds.t * Genarg.glob_generic_argument option + | NHole of Evar_kinds.t * Misctypes.intro_pattern_naming_expr * Genarg.glob_generic_argument option | NList of Id.t * Id.t * notation_constr * notation_constr * bool (** Part only in [glob_constr] *) | NLambda of Name.t * notation_constr * notation_constr diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index f47eb1c09..a0384faf8 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -46,7 +46,7 @@ open Egramml (** Declare Notations grammar rules *) let constr_expr_of_name (loc,na) = match na with - | Anonymous -> CHole (loc,None,None) + | Anonymous -> CHole (loc,None,Misctypes.IntroAnonymous,None) | Name id -> CRef (Ident (loc,id), None) let cases_pattern_expr_of_name (loc,na) = match na with diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 0c1c20ec6..49c0cd79c 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -37,20 +37,20 @@ let mk_cast = function let loc = Loc.merge (constr_loc c) (constr_loc ty) in CCast(loc, c, CastConv ty) +let binder_of_name expl (loc,na) = + LocalRawAssum ([loc, na], Default expl, + CHole (loc, Some (Evar_kinds.BinderType na), IntroAnonymous, None)) + let binders_of_names l = - List.map (fun (loc, na) -> - LocalRawAssum ([loc, na], Default Explicit, - CHole (loc, Some (Evar_kinds.BinderType na), None))) l + List.map (binder_of_name Explicit) l let binders_of_lidents l = - List.map (fun (loc, id) -> - LocalRawAssum ([loc, Name id], Default Explicit, - CHole (loc, Some (Evar_kinds.BinderType (Name id)), None))) l + List.map (fun (loc, id) -> binder_of_name Explicit (loc, Name id)) l let mk_fixb (id,bl,ann,body,(loc,tyc)) = let ty = match tyc with Some ty -> ty - | None -> CHole (loc, None, None) in + | None -> CHole (loc, None, IntroAnonymous, None) in (id,ann,bl,ty,body) let mk_cofixb (id,bl,ann,body,(loc,tyc)) = @@ -60,7 +60,7 @@ let mk_cofixb (id,bl,ann,body,(loc,tyc)) = Pp.str"Annotation forbidden in cofix expression.")) (fst ann) in let ty = match tyc with Some ty -> ty - | None -> CHole (loc, None, None) in + | None -> CHole (loc, None, IntroAnonymous, None) in (id,bl,ty,body) let mk_fix(loc,kw,id,dcls) = @@ -220,7 +220,7 @@ GEXTEND Gram CGeneralization (!@loc, Explicit, None, c) | "$("; tac = Tactic.tactic; ")$" -> let arg = Genarg.in_gen (Genarg.rawwit Constrarg.wit_tactic) tac in - CHole (!@loc, None, Some arg) + CHole (!@loc, None, IntroAnonymous, Some arg) ] ] ; forall: @@ -288,7 +288,9 @@ GEXTEND Gram | s=sort -> CSort (!@loc,s) | n=INT -> CPrim (!@loc, Numeral (Bigint.of_string n)) | s=string -> CPrim (!@loc, String s) - | "_" -> CHole (!@loc, None, None) + | "_" -> CHole (!@loc, None, IntroAnonymous, None) + | "?["; id=ident; "]" -> CHole (!@loc, None, IntroIdentifier id, None) + | "?["; id=pattern_ident; "]" -> CHole (!@loc, None, IntroFresh id, None) | id=pattern_ident; inst = evar_instance -> CEvar(!@loc,id,inst) ] ] ; inst: @@ -397,13 +399,13 @@ GEXTEND Gram | s = string -> CPatPrim (!@loc, String s) ] ] ; impl_ident_tail: - [ [ "}" -> fun id -> LocalRawAssum([id], Default Implicit, CHole(!@loc, None, None)) - | idl=LIST1 name; ":"; c=lconstr; "}" -> - (fun id -> LocalRawAssum (id::idl,Default Implicit,c)) - | idl=LIST1 name; "}" -> - (fun id -> LocalRawAssum (id::idl,Default Implicit,CHole (!@loc, None, None))) + [ [ "}" -> binder_of_name Implicit + | nal=LIST1 name; ":"; c=lconstr; "}" -> + (fun na -> LocalRawAssum (na::nal,Default Implicit,c)) + | nal=LIST1 name; "}" -> + (fun na -> LocalRawAssum (na::nal,Default Implicit,CHole (Loc.join_loc (fst na) !@loc, Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None))) | ":"; c=lconstr; "}" -> - (fun id -> LocalRawAssum ([id],Default Implicit,c)) + (fun na -> LocalRawAssum ([na],Default Implicit,c)) ] ] ; fixannot: @@ -413,9 +415,12 @@ GEXTEND Gram rel=OPT constr; "}" -> (id, CMeasureRec (m,rel)) ] ] ; + impl_name_head: + [ [ id = impl_ident_head -> (!@loc,Name id) ] ] + ; binders_fixannot: - [ [ id = impl_ident_head; assum = impl_ident_tail; bl = binders_fixannot -> - (assum (!@loc, Name id) :: fst bl), snd bl + [ [ na = impl_name_head; assum = impl_ident_tail; bl = binders_fixannot -> + (assum na :: fst bl), snd bl | f = fixannot -> [], f | b = binder; bl = binders_fixannot -> b @ fst bl, snd bl | -> [], (None, CStructRec) @@ -432,7 +437,7 @@ GEXTEND Gram binders_of_names (id::idl) @ bl | id1 = name; ".."; id2 = name -> [LocalRawAssum ([id1;(!@loc,Name ldots_var);id2], - Default Explicit,CHole (!@loc, None, None))] + Default Explicit,CHole (!@loc, None, IntroAnonymous, None))] | bl = closed_binder; bl' = binders -> bl@bl' ] ] @@ -441,7 +446,7 @@ GEXTEND Gram [ [ l = LIST0 binder -> List.flatten l ] ] ; binder: - [ [ id = name -> [LocalRawAssum ([id],Default Explicit,CHole (!@loc, None, None))] + [ [ id = name -> [LocalRawAssum ([id],Default Explicit,CHole (!@loc, None, IntroAnonymous, None))] | bl = closed_binder -> bl ] ] ; closed_binder: @@ -454,13 +459,13 @@ GEXTEND Gram | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" -> [LocalRawDef (id,CCast (Loc.merge (constr_loc t) (!@loc),c, CastConv t))] | "{"; id=name; "}" -> - [LocalRawAssum ([id],Default Implicit,CHole (!@loc, None, None))] + [LocalRawAssum ([id],Default Implicit,CHole (!@loc, None, IntroAnonymous, None))] | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" -> [LocalRawAssum (id::idl,Default Implicit,c)] | "{"; id=name; ":"; c=lconstr; "}" -> [LocalRawAssum ([id],Default Implicit,c)] | "{"; id=name; idl=LIST1 name; "}" -> - List.map (fun id -> LocalRawAssum ([id],Default Implicit,CHole (!@loc, None, None))) (id::idl) + List.map (fun id -> LocalRawAssum ([id],Default Implicit,CHole (!@loc, None, IntroAnonymous, None))) (id::idl) | "`("; tc = LIST1 typeclass_constraint SEP "," ; ")" -> List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Explicit, b), t)) tc | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" -> diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index d8620a0f2..de8d332b8 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -202,7 +202,7 @@ GEXTEND Gram | CCast (loc, t, (CastConv ty | CastVM ty | CastNative ty)) -> Term t, Some (Term ty) | _ -> mpv, None) | _ -> mpv, None - in Def (na, t, Option.default (Term (CHole (Loc.ghost, None, None))) ty) + in Def (na, t, Option.default (Term (CHole (Loc.ghost, None, IntroAnonymous, None))) ty) ] ] ; match_context_rule: diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 4b9d223ad..3e83e2ca1 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -429,7 +429,7 @@ GEXTEND Gram | -> true ]] ; simple_binder: - [ [ na=name -> ([na],Default Explicit,CHole (!@loc, None, None)) + [ [ na=name -> ([na],Default Explicit,CHole (!@loc, Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None)) | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> (nal,Default Explicit,c) ] ] ; diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index cabb09dc3..17fbd85cc 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -336,7 +336,7 @@ GEXTEND Gram ; type_cstr: [ [ ":"; c=lconstr -> c - | -> CHole (!@loc, None, None) ] ] + | -> CHole (!@loc, None, Misctypes.IntroAnonymous, None) ] ] ; (* Inductive schemes *) scheme: @@ -385,7 +385,7 @@ GEXTEND Gram (None,DefExpr(id,mkCLambdaN (!@loc) l b,None)) ] ] ; record_binder: - [ [ id = name -> (None,AssumExpr(id,CHole (!@loc, None, None))) + [ [ id = name -> (None,AssumExpr(id,CHole (!@loc, None, Misctypes.IntroAnonymous, None))) | id = name; f = record_binder_body -> f id ] ] ; assum_list: @@ -404,7 +404,7 @@ GEXTEND Gram t= [ coe = of_type_with_opt_coercion; c = lconstr -> fun l id -> (not (Option.is_empty coe),(id,mkCProdN (!@loc) l c)) | -> - fun l id -> (false,(id,mkCProdN (!@loc) l (CHole (!@loc, None, None)))) ] + fun l id -> (false,(id,mkCProdN (!@loc) l (CHole (!@loc, None, Misctypes.IntroAnonymous, None)))) ] -> t l ]] ; diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index e77ba3c58..5d26153d3 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -186,7 +186,7 @@ let interp_constr_or_thesis check_sort env sigma = function let abstract_one_hyp inject h glob = match h with Hvar (loc,(id,None)) -> - GProd (Loc.ghost,Name id, Explicit, GHole (loc,Evar_kinds.BinderType (Name id), None), glob) + GProd (Loc.ghost,Name id, Explicit, GHole (loc,Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), glob) | Hvar (loc,(id,Some typ)) -> GProd (Loc.ghost,Name id, Explicit, fst typ, glob) | Hprop st -> @@ -244,7 +244,7 @@ let rec glob_of_pat = let rec add_params n q = if n<=0 then q else add_params (pred n) (GHole(Loc.ghost, - Evar_kinds.TomatchTypeParameter(ind,n), None)::q) in + Evar_kinds.TomatchTypeParameter(ind,n), Misctypes.IntroAnonymous, None)::q) in let args = List.map glob_of_pat lpat in glob_app(loc,GRef(Loc.ghost,Globnames.ConstructRef cstr,None), add_params mind.Declarations.mind_nparams args) @@ -253,14 +253,14 @@ let prod_one_hyp = function (loc,(id,None)) -> (fun glob -> GProd (Loc.ghost,Name id, Explicit, - GHole (loc,Evar_kinds.BinderType (Name id), None), glob)) + GHole (loc,Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), glob)) | (loc,(id,Some typ)) -> (fun glob -> GProd (Loc.ghost,Name id, Explicit, fst typ, glob)) let prod_one_id (loc,id) glob = GProd (Loc.ghost,Name id, Explicit, - GHole (loc,Evar_kinds.BinderType (Name id), None), glob) + GHole (loc,Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), glob) let let_in_one_alias (id,pat) glob = GLetIn (Loc.ghost,Name id, glob_of_pat pat, glob) @@ -341,7 +341,7 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps = GVar (loc,id)) params in let dum_args= List.init oib.Declarations.mind_nrealargs - (fun _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark (Evar_kinds.Define false),None)) in + (fun _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark (Evar_kinds.Define false),Misctypes.IntroAnonymous, None)) in glob_app(Loc.ghost,rind,rparams@rparams_rec@dum_args) in let pat_vars,aliases,patt = interp_pattern env pat in let inject = function @@ -416,7 +416,7 @@ let abstract_one_arg = function (loc,(id,None)) -> (fun glob -> GLambda (Loc.ghost,Name id, Explicit, - GHole (loc,Evar_kinds.BinderType (Name id),None), glob)) + GHole (loc,Evar_kinds.BinderType (Name id),Misctypes.IntroAnonymous,None), glob)) | (loc,(id,Some typ)) -> (fun glob -> GLambda (Loc.ghost,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 a5f28003c..41d93fc4f 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -1274,7 +1274,7 @@ let understand_my_constr c gls = let env = pf_env gls in let rawc = Detyping.detype false [] env Evd.empty c in let rec frob = function - | GEvar _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark Evar_kinds.Expand,None) + | GEvar _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark Evar_kinds.Expand,Misctypes.IntroAnonymous,None) | rc -> map_glob_constr frob rc in Pretyping.understand_tcc env (sig_sig gls) ~expected_type:(Pretyping.OfType (pf_concl gls)) (frob rawc) diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 80576212f..0aafafde9 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -124,7 +124,7 @@ let mk_open_instance id idc gl m t= match t with GLambda(loc,name,k,_,t0)-> let t1=raux (n-1) t0 in - GLambda(loc,name,k,GHole (Loc.ghost,Evar_kinds.BinderType name,None),t1) + GLambda(loc,name,k,GHole (Loc.ghost,Evar_kinds.BinderType name,Misctypes.IntroAnonymous,None),t1) | _-> anomaly (Pp.str "can't happen") in let ntt=try fst (Pretyping.understand env evmap (raux m rawt))(*FIXME*) diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index e55ede968..291f835ee 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -18,7 +18,7 @@ let mkGProd(n,t,b) = GProd(Loc.ghost,n,Explicit,t,b) let mkGLetIn(n,t,b) = GLetIn(Loc.ghost,n,t,b) let mkGCases(rto,l,brl) = GCases(Loc.ghost,Term.RegularStyle,rto,l,brl) let mkGSort s = GSort(Loc.ghost,s) -let mkGHole () = GHole(Loc.ghost,Evar_kinds.BinderType Anonymous,None) +let mkGHole () = GHole(Loc.ghost,Evar_kinds.BinderType Anonymous,Misctypes.IntroAnonymous,None) let mkGCast(b,t) = GCast(Loc.ghost,b,CastConv t) (* diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml index a6b3d9038..2a0016df9 100644 --- a/plugins/syntax/numbers_syntax.ml +++ b/plugins/syntax/numbers_syntax.ml @@ -165,10 +165,10 @@ let word_of_pos_bigint dloc hght n = if hgt <= 0 then int31_of_pos_bigint dloc n else if equal n zero then - GApp (dloc, ref_W0, [GHole (dloc, Evar_kinds.InternalHole, None)]) + GApp (dloc, ref_W0, [GHole (dloc, Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None)]) else let (h,l) = split_at hgt n in - GApp (dloc, ref_WW, [GHole (dloc, Evar_kinds.InternalHole, None); + GApp (dloc, ref_WW, [GHole (dloc, Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None); decomp (hgt-1) h; decomp (hgt-1) l]) in diff --git a/pretyping/cases.ml b/pretyping/cases.ml index c9c6cecb1..d52830a16 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1946,7 +1946,7 @@ let mk_JMeq evdref typ x typ' y = let mk_JMeq_refl evdref typ x = papp evdref coq_JMeq_refl [| typ; x |] -let hole = GHole (Loc.ghost, Evar_kinds.QuestionMark (Evar_kinds.Define true), None) +let hole = GHole (Loc.ghost, Evar_kinds.QuestionMark (Evar_kinds.Define true), Misctypes.IntroAnonymous, None) let constr_of_pat env evdref arsign pat avoid = let rec typ env (ty, realargs) pat avoid = diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 0b0ff2fb5..df3d243f1 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -737,7 +737,7 @@ let rec subst_glob_constr subst raw = | GSort _ -> raw - | GHole (loc, knd, solve) -> + | GHole (loc, knd, naming, solve) -> let nknd = match knd with | Evar_kinds.ImplicitArg (ref, i, b) -> let nref, _ = subst_global subst ref in @@ -746,7 +746,7 @@ let rec subst_glob_constr subst raw = in let nsolve = Option.smartmap (Hook.get f_subst_genarg subst) solve in if nsolve == solve && nknd == knd then raw - else GHole (loc, nknd, nsolve) + else GHole (loc, nknd, naming, nsolve) | GCast (loc,r1,k) -> let r1' = subst_glob_constr subst r1 in diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 64bdb90a2..cebb45266 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -358,35 +358,35 @@ let new_pure_evar_full evd evi = let evd = Evd.add evd evk evi in (evd, evk) -let new_pure_evar sign evd ?(src=default_source) ?filter ?candidates ?store typ = +let new_pure_evar sign evd ?(src=default_source) ?filter ?candidates ?store ?(naming=Misctypes.IntroAnonymous) typ = let newevk = new_untyped_evar() in - let evd = evar_declare sign newevk typ ~src ?filter ?candidates ?store evd in + let evd = evar_declare sign newevk typ ~src ?filter ?candidates ?store ~naming evd in (evd,newevk) -let new_evar_instance sign evd typ ?src ?filter ?candidates ?store instance = +let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?(naming=Misctypes.IntroAnonymous) instance = assert (not !Flags.debug || List.distinct (ids_of_named_context (named_context_of_val sign))); - let evd,newevk = new_pure_evar sign evd ?src ?filter ?candidates ?store typ in + let evd,newevk = new_pure_evar sign evd ?src ?filter ?candidates ?store ~naming typ in (evd,mkEvar (newevk,Array.of_list instance)) (* [new_evar] declares a new existential in an env env with type typ *) (* Converting the env into the sign of the evar to define *) -let new_evar env evd ?src ?filter ?candidates ?store typ = +let new_evar env evd ?src ?filter ?candidates ?store ?(naming=Misctypes.IntroAnonymous) typ = let sign,typ',instance,subst,vsubst = push_rel_context_to_named_context env typ in let candidates = Option.map (List.map (subst2 subst vsubst)) candidates in let instance = match filter with | None -> instance | Some filter -> Filter.filter_list filter instance in - new_evar_instance sign evd typ' ?src ?filter ?candidates ?store instance + new_evar_instance sign evd typ' ?src ?filter ?candidates ?store ~naming instance -let new_type_evar env evd ?src ?filter rigid = +let new_type_evar env evd ?src ?filter ?(naming=Misctypes.IntroAnonymous) rigid = let evd', s = new_sort_variable rigid evd in - let evd', e = new_evar env evd' ?src ?filter (mkSort s) in + let evd', e = new_evar env evd' ?src ?filter ~naming (mkSort s) in evd', (e, s) -let e_new_type_evar env evdref ?src ?filter rigid = - let evd', c = new_type_evar env !evdref ?src ?filter rigid in +let e_new_type_evar env evdref ?src ?filter ?(naming=Misctypes.IntroAnonymous) rigid = + let evd', c = new_type_evar env !evdref ?src ?filter ~naming rigid in evdref := evd'; c @@ -399,8 +399,8 @@ let e_new_Type ?(rigid=Evd.univ_flexible) env evdref = evdref := evd'; mkSort s (* The same using side-effect *) -let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ty = - let (evd',ev) = new_evar env !evdref ~src:src ?filter ?candidates ?store ty in +let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?(naming=Misctypes.IntroAnonymous) ty = + let (evd',ev) = new_evar env !evdref ~src:src ?filter ?candidates ?store ~naming ty in evdref := evd'; ev diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 8a07cce5d..de55a643a 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -23,27 +23,32 @@ val mk_new_meta : unit -> constr (** {6 Creating a fresh evar given their type and context} *) val new_evar : env -> evar_map -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> - ?candidates:constr list -> ?store:Store.t -> types -> evar_map * constr + ?candidates:constr list -> ?store:Store.t -> + ?naming:Misctypes.intro_pattern_naming_expr -> types -> evar_map * constr val new_pure_evar : named_context_val -> evar_map -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> - ?candidates:constr list -> ?store:Store.t -> types -> evar_map * evar + ?candidates:constr list -> ?store:Store.t -> + ?naming:Misctypes.intro_pattern_naming_expr -> types -> evar_map * evar val new_pure_evar_full : evar_map -> evar_info -> evar_map * evar (** the same with side-effects *) val e_new_evar : env -> evar_map ref -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> - ?candidates:constr list -> ?store:Store.t -> types -> constr + ?candidates:constr list -> ?store:Store.t -> + ?naming:Misctypes.intro_pattern_naming_expr -> types -> constr (** Create a new Type existential variable, as we keep track of them during type-checking and unification. *) val new_type_evar : - env -> evar_map -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> rigid -> + env -> evar_map -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> + ?naming:Misctypes.intro_pattern_naming_expr -> rigid -> evar_map * (constr * sorts) val e_new_type_evar : env -> evar_map ref -> - ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> rigid -> constr * sorts + ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> + ?naming:Misctypes.intro_pattern_naming_expr -> rigid -> constr * sorts val new_Type : ?rigid:rigid -> env -> evar_map -> evar_map * constr val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr @@ -65,7 +70,8 @@ val e_new_global : evar_map ref -> Globnames.global_reference -> constr val new_evar_instance : named_context_val -> evar_map -> types -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list -> - ?store:Store.t -> constr list -> evar_map * constr + ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> + constr list -> evar_map * constr val make_pure_subst : evar_info -> constr array -> (Id.t * constr) list diff --git a/pretyping/evd.ml b/pretyping/evd.ml index fd104d847..ffc1ea2a7 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -599,16 +599,28 @@ let progress_evar_map d1 d2 = in not (d1 == d2) && EvMap.exists is_new d1.undf_evars -let add_name_newly_undefined evk evi (evtoid,idtoev) = - let id = evar_ident_info evi in - let id = Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) in - (EvMap.add evk id evtoid, Idmap.add id evk idtoev) - -let add_name_undefined evk evi (evtoid,idtoev as evar_names) = +let add_name_newly_undefined naming evk evi (evtoid,idtoev) = + let id = match naming with + | Misctypes.IntroAnonymous -> + let id = evar_ident_info evi in + Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) + | Misctypes.IntroIdentifier id -> + let id' = + Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) in + if not (Names.Id.equal id id') then + user_err_loc + (Loc.ghost,"",str "Already an existential evar of name " ++ pr_id id); + id' + | Misctypes.IntroFresh id -> + Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) + | Misctypes.IntroWildcard -> assert false in + (EvMap.add evk id evtoid, Idmap.add id evk idtoev) + +let add_name_undefined naming evk evi (evtoid,idtoev as evar_names) = if EvMap.mem evk evtoid then evar_names else - add_name_newly_undefined evk evi evar_names + add_name_newly_undefined naming evk evi evar_names let remove_name_defined evk (evtoid,idtoev) = let id = EvMap.find evk evtoid in @@ -618,6 +630,14 @@ let remove_name_possibly_already_defined evk evar_names = try remove_name_defined evk evar_names with Not_found -> evar_names +let rename evk id evd = + let (evtoid,idtoev) = evd.evar_names in + let id' = EvMap.find evk evtoid in + if Idmap.mem id idtoev then anomaly (str "Evar name already in use"); + { evd with evar_names = + (EvMap.add evk id evtoid (* overwrite old name *), + Idmap.add id evk (Idmap.remove id' idtoev)) } + let reassign_name_defined evk evk' (evtoid,idtoev) = let id = EvMap.find evk evtoid in (EvMap.add evk' id (EvMap.remove evk evtoid), @@ -625,7 +645,7 @@ let reassign_name_defined evk evk' (evtoid,idtoev) = let add d e i = match i.evar_body with | Evar_empty -> - let evar_names = add_name_undefined e i d.evar_names in + let evar_names = add_name_undefined Misctypes.IntroAnonymous e i d.evar_names in { d with undf_evars = EvMap.add e i d.undf_evars; evar_names } | Evar_defined _ -> let evar_names = remove_name_possibly_already_defined e d.evar_names in @@ -839,7 +859,8 @@ let define evk body evd = { evd with defn_evars; undf_evars; last_mods; evar_names } let evar_declare hyps evk ty ?(src=(Loc.ghost,Evar_kinds.InternalHole)) - ?(filter=Filter.identity) ?candidates ?(store=Store.empty) evd = + ?(filter=Filter.identity) ?candidates ?(store=Store.empty) + ?(naming=Misctypes.IntroAnonymous) evd = let () = match Filter.repr filter with | None -> () | Some filter -> @@ -854,7 +875,7 @@ let evar_declare hyps evk ty ?(src=(Loc.ghost,Evar_kinds.InternalHole)) evar_candidates = candidates; evar_extra = store; } in - let evar_names = add_name_newly_undefined evk evar_info evd.evar_names in + let evar_names = add_name_newly_undefined naming evk evar_info evd.evar_names in { evd with undf_evars = EvMap.add evk evar_info evd.undf_evars; evar_names } let restrict evk evk' filter ?candidates evd = @@ -1018,7 +1039,7 @@ let merge_names evar_names def' undef' = EvMap.fold (fun n _ evar_names -> remove_name_possibly_already_defined n evar_names) def' evar_names in - EvMap.fold add_name_undefined undef' evar_names + EvMap.fold (add_name_undefined Misctypes.IntroAnonymous) undef' evar_names let merge_metas metas1 metas2 = List.fold_left (fun m (n,v) -> Metamap.add n v m) diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 22768fb69..467e1a163 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -246,8 +246,8 @@ val evars_reset_evd : ?with_conv_pbs:bool -> ?with_univs:bool -> val evar_declare : named_context_val -> evar -> types -> ?src:Loc.t * Evar_kinds.t -> - ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> - evar_map -> evar_map + ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> + ?naming:Misctypes.intro_pattern_naming_expr -> evar_map -> evar_map (** Convenience function. Just a wrapper around {!add}. *) val restrict : evar -> evar -> Filter.t -> ?candidates:constr list -> @@ -259,6 +259,8 @@ val evar_source : existential_key -> evar_map -> Evar_kinds.t located val evar_ident : existential_key -> evar_map -> Id.t +val rename : existential_key -> Id.t -> evar_map -> evar_map + val evar_key : Id.t -> evar_map -> existential_key val evar_source_of_meta : metavariable -> evar_map -> Evar_kinds.t located diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 9157cdb81..fd51545b2 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -96,8 +96,9 @@ let rec glob_constr_eq c1 c2 = match c1, c2 with Array.equal glob_constr_eq c1 c2 && Array.equal glob_constr_eq t1 t2 | GSort (_, s1), GSort (_, s2) -> Miscops.glob_sort_eq s1 s2 -| GHole (_, kn1, gn1), GHole (_, kn2, gn2) -> - Option.equal (==) gn1 gn2 (** Only thing sensible *) +| GHole (_, kn1, nam1, gn1), GHole (_, kn2, nam2, gn2) -> + Option.equal (==) gn1 gn2 (** Only thing sensible *) && + Miscops.intro_pattern_naming_eq nam1 nam2 | GCast (_, c1, t1), GCast (_, c2, t2) -> glob_constr_eq c1 c2 && cast_type_eq glob_constr_eq t1 t2 | _ -> false @@ -342,7 +343,7 @@ let loc_of_glob_constr = function | GIf (loc,_,_,_,_) -> loc | GRec (loc,_,_,_,_,_) -> loc | GSort (loc,_) -> loc - | GHole (loc,_,_) -> loc + | GHole (loc,_,_,_) -> loc | GCast (loc,_,_) -> loc (**********************************************************************) @@ -356,7 +357,7 @@ let rec cases_pattern_of_glob_constr na = function raise Not_found | Anonymous -> PatVar (loc,Name id) end - | GHole (loc,_,_) -> PatVar (loc,na) + | GHole (loc,_,_,_) -> PatVar (loc,na) | GRef (loc,ConstructRef cstr,_) -> PatCstr (loc,cstr,[],na) | GApp (loc,GRef (_,ConstructRef cstr,_),l) -> diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml index 5b5bbe095..e96e3a8b7 100644 --- a/pretyping/miscops.ml +++ b/pretyping/miscops.ml @@ -30,3 +30,10 @@ let glob_sort_eq g1 g2 = match g1, g2 with | GSet, GSet -> true | GType l1, GType l2 -> List.for_all2 CString.equal l1 l2 | _ -> false + +let intro_pattern_naming_eq nam1 nam2 = match nam1, nam2 with +| IntroAnonymous, IntroAnonymous -> true +| IntroIdentifier id1, IntroIdentifier id2 -> Names.Id.equal id1 id2 +| IntroWildcard, IntroWildcard -> true +| IntroFresh id1, IntroFresh id2 -> Names.Id.equal id1 id2 +| _ -> false diff --git a/pretyping/miscops.mli b/pretyping/miscops.mli index 84541a3b2..6235533d7 100644 --- a/pretyping/miscops.mli +++ b/pretyping/miscops.mli @@ -16,3 +16,8 @@ val smartmap_cast_type : ('a -> 'a) -> 'a cast_type -> 'a cast_type (** Equalities on [glob_sort] *) val glob_sort_eq : glob_sort -> glob_sort -> bool + +(** Equalities on [intro_pattern_naming] *) + +val intro_pattern_naming_eq : + intro_pattern_naming_expr -> intro_pattern_naming_expr -> bool diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 4a1dc1dd6..3e43853a5 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -355,7 +355,7 @@ let rec pat_of_raw metas vars = function 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,Evar_kinds.InternalHole, None),c) in + GLambda (loc,na,Explicit,GHole (loc,Evar_kinds.InternalHole, IntroAnonymous, None),c) in let c = List.fold_left mkGLambda c nal in let cip = { cip_style = LetStyle; diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 8c4dbfd98..69aee0a60 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -440,15 +440,15 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var let k = Evar_kinds.MatchingVar (someta,n) in { uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty } - | GHole (loc, k, None) -> + | GHole (loc, k, naming, None) -> let ty = match tycon with | Some ty -> ty | None -> new_type_evar env evdref loc in - { uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty } + { uj_val = e_new_evar env evdref ~src:(loc,k) ~naming ty; uj_type = ty } - | GHole (loc, k, Some arg) -> + | GHole (loc, k, _naming, Some arg) -> let ty = match tycon with | Some ty -> ty @@ -910,7 +910,7 @@ and pretype_instance resolve_tc env evdref lvar loc hyps evk update = (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *) and pretype_type resolve_tc valcon env evdref lvar = function - | GHole (loc, knd, None) -> + | GHole (loc, knd, naming, None) -> (match valcon with | Some v -> let s = @@ -926,7 +926,7 @@ and pretype_type resolve_tc valcon env evdref lvar = function utj_type = s } | None -> let s = evd_comb0 (new_sort_variable univ_flexible_alg) evdref in - { utj_val = e_new_evar env evdref ~src:(loc, knd) (mkSort s); + { utj_val = e_new_evar env evdref ~src:(loc, knd) ~naming (mkSort s); utj_type = s}) | c -> let j = pretype resolve_tc empty_tycon env evdref lvar c in diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index e1f41e381..c49bdf5f4 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -149,11 +149,11 @@ let pr_expl_args pr (a,expl) = str "(" ++ pr_id id ++ str ":=" ++ pr ltop a ++ str ")" let pr_opt_type pr = function - | CHole _ -> mt () + | CHole (_,_,Misctypes.IntroAnonymous,_) -> mt () | t -> cut () ++ str ":" ++ pr t let pr_opt_type_spc pr = function - | CHole _ -> mt () + | CHole (_,_,Misctypes.IntroAnonymous,_) -> mt () | t -> str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t let pr_lident (loc,id) = @@ -265,7 +265,7 @@ let pr_binder many pr (nal,k,t) = end | Default b -> match t with - | CHole _ -> + | CHole (_,_,Misctypes.IntroAnonymous,_) -> let s = prlist_with_sep spc pr_lname nal in hov 1 (surround_implicit b s) | _ -> @@ -278,7 +278,7 @@ let pr_binder_among_many pr_c = function | LocalRawDef (na,c) -> let c,topt = match c with | CCast(_,c, (CastConv t|CastVM t|CastNative t)) -> c, t - | _ -> c, CHole (Loc.ghost, None, None) in + | _ -> c, CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None) in surround (pr_lname na ++ pr_opt_type pr_c topt ++ str":=" ++ cut() ++ pr_c c) @@ -403,7 +403,7 @@ let pr_case_item pr (tm,asin) = let pr_case_type pr po = match po with - | None | Some (CHole _) -> mt() + | None | Some (CHole (_,_,Misctypes.IntroAnonymous,_)) -> mt() | Some p -> spc() ++ hov 2 (str "return" ++ pr_sep_com spc (pr lsimpleconstr) p) @@ -552,7 +552,11 @@ let pr pr sep inherited a = hov 0 (str "else" ++ pr (fun () -> brk (1,1)) ltop b2)), lif - | CHole _ -> str "_", latom + | CHole (_,_,Misctypes.IntroIdentifier id,_) -> + str "?[" ++ pr_id id ++ str "]", latom + | CHole (_,_,Misctypes.IntroFresh id,_) -> + str "?[?" ++ pr_id id ++ str "]", latom + | CHole (_,_,_,_) -> str "_", latom | CEvar (_,n,l) -> pr_evar (pr mt) n l, latom | CPatVar (_,p) -> str "?" ++ pr_patvar p, latom | CSort (_,s) -> pr_glob_sort s, latom diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index b841c19cc..a5235a25f 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -236,7 +236,7 @@ let pr_module_binders l pr_c = prlist_strict (pr_module_vardecls pr_c) l let pr_type_option pr_c = function - | CHole (loc, k, _) -> mt() + | CHole (loc, k, Misctypes.IntroAnonymous, _) -> mt() | _ as c -> brk(0,2) ++ str" :" ++ pr_c c let pr_decl_notation prc ((loc,ntn),c,scopt) = diff --git a/proofs/goal.ml b/proofs/goal.ml index ce7f5959a..631c2428e 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -22,7 +22,7 @@ type goal = { logical information once put together with an evar_map. *) tags : string list; - (** Heriditary? tags to be displayed *) + (** Hereditary? tags to be displayed *) cache : Evd.evar_map; (** Invariant: for all sigma, if gl.cache == sigma and gl.content is actually pertaining to sigma, then gl is nf-evarized in sigma. We use this not to @@ -246,6 +246,11 @@ module V82 = struct let partial_solution sigma { content=evk } c = Evd.define evk c sigma + (* Instantiates a goal with an open term, using name of goal for evk' *) + let partial_solution_to sigma { content=evk } { content=evk' } c = + let id = Evd.evar_ident evk sigma in + Evd.rename evk' id (Evd.define evk c sigma) + (* Parts of the progress tactical *) let same_goal evars1 gl1 evars2 gl2 = let evi1 = content evars1 gl1 in diff --git a/proofs/goal.mli b/proofs/goal.mli index 4d4d0c2eb..d31a51fbd 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -94,10 +94,13 @@ module V82 : sig stuff. *) val build : Evd.evar -> goal - (* Instantiates a goal with an open term *) val partial_solution : Evd.evar_map -> goal -> Term.constr -> Evd.evar_map - + + (* Instantiates a goal with an open term, reusing name of goal for + second goal *) + val partial_solution_to : Evd.evar_map -> goal -> goal -> Term.constr -> Evd.evar_map + (* Principal part of the weak-progress tactical *) val weak_progress : goal list Evd.sigma -> goal Evd.sigma -> bool diff --git a/proofs/logic.ml b/proofs/logic.ml index b9cff0527..008df0096 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -530,14 +530,14 @@ let prim_refiner r sigma goal = let (sg,ev,sigma) = mk_goal (push_named_context_val (id,None,c1) sign) (subst1 (mkVar id) b) in let sigma = - Goal.V82.partial_solution sigma goal (mkNamedLambda id c1 ev) in + Goal.V82.partial_solution_to sigma goal sg (mkNamedLambda id c1 ev) in ([sg], sigma) | LetIn (_,c1,t1,b) -> let (sg,ev,sigma) = mk_goal (push_named_context_val (id,Some c1,t1) sign) (subst1 (mkVar id) b) in let sigma = - Goal.V82.partial_solution sigma goal (mkNamedLetIn id c1 t1 ev) in + Goal.V82.partial_solution_to sigma goal sg (mkNamedLetIn id c1 t1 ev) in ([sg], sigma) | _ -> raise (RefinerError IntroNeedsProduct)) @@ -559,7 +559,7 @@ let prim_refiner r sigma goal = let (sg2,ev2,sigma) = Goal.V82.mk_goal sigma sign cl (Goal.V82.extra sigma goal) in let oterm = Term.mkApp (mkNamedLambda id t ev2 , [| ev1 |]) in - let sigma = Goal.V82.partial_solution sigma goal oterm in + let sigma = Goal.V82.partial_solution_to sigma goal sg2 oterm in if b then ([sg1;sg2],sigma) else ([sg2;sg1],sigma) | FixRule (f,n,rest,j) -> @@ -661,12 +661,12 @@ let prim_refiner r sigma goal = let (sg,ev,sigma) = mk_goal sign cl' in let sigma = check_conv_leq_goal env sigma cl' cl' cl in let ev = if k != DEFAULTcast then mkCast(ev,k,cl) else ev in - let sigma = Goal.V82.partial_solution sigma goal ev in + let sigma = Goal.V82.partial_solution_to sigma goal sg ev in ([sg], sigma) | Convert_hyp (id,copt,ty) -> let (gl,ev,sigma) = mk_goal (convert_hyp sign sigma (id,copt,ty)) cl in - let sigma = Goal.V82.partial_solution sigma goal ev in + let sigma = Goal.V82.partial_solution_to sigma goal gl ev in ([gl], sigma) (* And now the structural rules *) @@ -676,7 +676,7 @@ let prim_refiner r sigma goal = let (gl,ev,sigma) = Goal.V82.mk_goal nsigma hyps concl (Goal.V82.extra nsigma goal) in - let sigma = Goal.V82.partial_solution sigma goal ev in + let sigma = Goal.V82.partial_solution_to sigma goal gl ev in ([gl], sigma) | Move (withdep, hfrom, hto) -> @@ -685,7 +685,7 @@ let prim_refiner r sigma goal = let hyps' = move_hyp withdep toleft (left,declfrom,right) hto in let (gl,ev,sigma) = mk_goal hyps' cl in - let sigma = Goal.V82.partial_solution sigma goal ev in + let sigma = Goal.V82.partial_solution_to sigma goal gl ev in ([gl], sigma) | Rename (id1,id2) -> @@ -698,5 +698,5 @@ let prim_refiner r sigma goal = let cl' = replace_vars [id1,mkVar id2] cl in let (gl,ev,sigma) = mk_goal sign' cl' in let ev = Vars.replace_vars [(id2,mkVar id1)] ev in - let sigma = Goal.V82.partial_solution sigma goal ev in + let sigma = Goal.V82.partial_solution_to sigma goal gl ev in ([gl], sigma) diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index 415ea951f..bd6f0fe9e 100644 --- a/stm/texmacspp.ml +++ b/stm/texmacspp.ml @@ -429,7 +429,7 @@ and pp_expr ?(attr=[]) e = (xmlOperator "evar" loc ~attr:["id", string_of_id ek] :: ppcel) | CPatVar (loc, id) -> xmlPatvar (string_of_id id) loc - | CHole (loc, _, _) -> xmlCst ~attr "_" loc + | CHole (loc, _, _, _) -> xmlCst ~attr "_" loc | CIf (loc, test, (_, ret), th, el) -> let return = match ret with | None -> [] diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 34f5b52eb..cb15bb94c 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -596,7 +596,8 @@ let subst_var_with_hole occ tid t = else (incr locref; GHole (Loc.make_loc (!locref,0), - Evar_kinds.QuestionMark(Evar_kinds.Define true), None))) + Evar_kinds.QuestionMark(Evar_kinds.Define true), + Misctypes.IntroAnonymous, None))) else x | c -> map_glob_constr_left_to_right substrec c in let t' = substrec t @@ -607,13 +608,13 @@ let subst_hole_with_term occ tc t = let locref = ref 0 in let occref = ref occ in let rec substrec = function - | GHole (_,Evar_kinds.QuestionMark(Evar_kinds.Define true),s) -> + | GHole (_,Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s) -> decr occref; if Int.equal !occref 0 then tc else (incr locref; GHole (Loc.make_loc (!locref,0), - Evar_kinds.QuestionMark(Evar_kinds.Define true),s)) + Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s)) | c -> map_glob_constr_left_to_right substrec c in substrec t diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 30ee5c514..bd2074139 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1766,7 +1766,7 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans = (Ident (Loc.ghost,Id.of_string "Equivalence_Symmetric"), lemma2); (Ident (Loc.ghost,Id.of_string "Equivalence_Transitive"), lemma3)]) -let cHole = CHole (Loc.ghost, None, None) +let cHole = CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None) let proper_projection r ty = let ctx, inst = decompose_prod_assum ty in diff --git a/toplevel/classes.ml b/toplevel/classes.ml index ad6c4236e..8f36fc79f 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -115,7 +115,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro (fun avoid (clname, (id, _, t)) -> match clname with | Some (cl, b) -> - let t = CHole (Loc.ghost, None, None) in + let t = CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None) in t, avoid | None -> failwith ("new instance: under-applied typeclass")) cl @@ -223,7 +223,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro k.cl_projs; c :: props, rest' with Not_found -> - (CHole (Loc.ghost, Some Evar_kinds.GoalEvar, None) :: props), rest + (CHole (Loc.ghost, Some Evar_kinds.GoalEvar, Misctypes.IntroAnonymous, None) :: props), rest else props, rest) ([], props) k.cl_props in diff --git a/toplevel/command.ml b/toplevel/command.ml index 95cfd73a0..a23b1b64a 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -53,7 +53,7 @@ let rec under_binders env f n c = let rec complete_conclusion a cs = function | CProdN (loc,bl,c) -> CProdN (loc,bl,complete_conclusion a cs c) | CLetIn (loc,b,t,c) -> CLetIn (loc,b,t,complete_conclusion a cs c) - | CHole (loc, k, _) -> + | CHole (loc, k, _, _) -> let (has_no_args,name,params) = a in if not has_no_args then user_err_loc (loc,"", diff --git a/toplevel/record.ml b/toplevel/record.ml index 7694869a5..be3fb7c2c 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -86,7 +86,7 @@ let compute_constructor_level evars env l = let binder_of_decl = function | Vernacexpr.AssumExpr(n,t) -> (n,None,t) - | Vernacexpr.DefExpr(n,c,t) -> (n,Some c, match t with Some c -> c | None -> CHole (fst n, None, None)) + | Vernacexpr.DefExpr(n,c,t) -> (n,Some c, match t with Some c -> c | None -> CHole (fst n, None, Misctypes.IntroAnonymous, None)) let binders_of_decls = List.map binder_of_decl -- cgit v1.2.3