From 962c99d0bf1261ac956611678480abe11d6d6803 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 6 May 2016 18:02:21 +0200
Subject: [PATCH] Let iIntros "*" reuse names of binders.

We may want to do the same for iIntros ? and iDestruct "H" as {?} "H",
but that requires more work. However, I do not think I want to rely on
names chosen this way.
---
 proofmode/tactics.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 035cf8fb1..7f3d22d44 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -570,7 +570,7 @@ Local Tactic Notation "iIntroForall" :=
   lazymatch goal with
   | |- âˆ€ _, ?P => fail
   | |- âˆ€ _, _ => intro
-  | |- _ âŠ¢ (âˆ€ _, _) => iIntro {?}
+  | |- _ âŠ¢ (âˆ€ x : _, _) => iIntro {x}
   end.
 Local Tactic Notation "iIntro" :=
   lazymatch goal with
-- 
GitLab