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.

6 files changed, 39 insertions, 39 deletions

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 _ ->