From 538b77dbb3b7799dc4d2e18033fc4fbf2eb26f7f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 30 Sep 2014 09:13:40 +0200
Subject: 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.
---
 pretyping/evd.mli | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'pretyping/evd.mli')

diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 22768fb69f..467e1a1636 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
-- 
cgit v1.2.3