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.

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