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.

11 files changed, 86 insertions, 44 deletions

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