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

(limited to 'tactics/rewrite.ml')

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