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.

5 files changed, 33 insertions, 28 deletions

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index f47eb1c091..a0384faf84 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 0c1c20ec65..49c0cd79c0 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 d8620a0f21..de8d332b8b 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 4b9d223ad7..3e83e2ca18 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 cabb09dc3e..17fbd85cc2 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
      ]]
 ;