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.

1 files changed, 12 insertions, 12 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 64bdb90a22..cebb45266b 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