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.
---
 tactics/extratactics.ml4 | 7 ++++---
 tactics/rewrite.ml       | 2 +-
 2 files changed, 5 insertions(+), 4 deletions(-)

(limited to 'tactics')

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 34f5b52ebf..cb15bb94c0 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -596,7 +596,8 @@ let subst_var_with_hole occ tid t =
            else
 	     (incr locref;
 	      GHole (Loc.make_loc (!locref,0),
-		     Evar_kinds.QuestionMark(Evar_kinds.Define true), None)))
+		     Evar_kinds.QuestionMark(Evar_kinds.Define true),
+                     Misctypes.IntroAnonymous, None)))
         else x
     | c -> map_glob_constr_left_to_right substrec c in
   let t' = substrec t
@@ -607,13 +608,13 @@ let subst_hole_with_term occ tc t =
   let locref = ref 0 in
   let occref = ref occ in
   let rec substrec = function
-    | GHole (_,Evar_kinds.QuestionMark(Evar_kinds.Define true),s) ->
+    | GHole (_,Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s) ->
         decr occref;
         if Int.equal !occref 0 then tc
         else
 	  (incr locref;
 	   GHole (Loc.make_loc (!locref,0),
-		  Evar_kinds.QuestionMark(Evar_kinds.Define true),s))
+		  Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s))
     | c -> map_glob_constr_left_to_right substrec c
   in
   substrec t
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 30ee5c5147..bd20741399 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1766,7 +1766,7 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans =
 	     (Ident (Loc.ghost,Id.of_string "Equivalence_Symmetric"), lemma2);
 	     (Ident (Loc.ghost,Id.of_string "Equivalence_Transitive"), lemma3)])
 
-let cHole = CHole (Loc.ghost, None, None)
+let cHole = CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None)
 
 let proper_projection r ty =
   let ctx, inst = decompose_prod_assum ty in
-- 
cgit v1.2.3