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.
---
 intf/notation_term.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'intf/notation_term.mli')

diff --git a/intf/notation_term.mli b/intf/notation_term.mli
index daf605ab28..5d9c1c177b 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
-- 
cgit v1.2.3