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/miscops.ml | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'pretyping/miscops.ml')

diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
index 5b5bbe095b..e96e3a8b7f 100644
--- a/pretyping/miscops.ml
+++ b/pretyping/miscops.ml
@@ -30,3 +30,10 @@ let glob_sort_eq g1 g2 = match g1, g2 with
 | GSet, GSet -> true
 | GType l1, GType l2 -> List.for_all2 CString.equal l1 l2
 | _ -> false
+
+let intro_pattern_naming_eq nam1 nam2 = match nam1, nam2 with
+| IntroAnonymous, IntroAnonymous -> true
+| IntroIdentifier id1, IntroIdentifier id2 -> Names.Id.equal id1 id2
+| IntroWildcard, IntroWildcard -> true
+| IntroFresh id1, IntroFresh id2 -> Names.Id.equal id1 id2
+| _ -> false
-- 
cgit v1.2.3