Make sure that `iIntros "*"` uses a fresh name.

6ff1c18a · Robbert Krebbers · 92024176 · 6ff1c18a
Commit 6ff1c18a authored Dec 27, 2016 by Robbert Krebbers
Hide whitespace changes
Inline Side-by-side

Showing with 1 addition and 1 deletion

theories/proofmode/tactics.v theories/proofmode/tactics.v +1 -1

No files found.
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -755,7 +755,7 @@ Local Tactic Notation "iIntroForall" :=
  lazymatch goal with
  | |- ∀ _, ?P => fail
  | |- ∀ _, _ => intro
-  | |- _ ⊢ (∀ x : _, _) => iIntro (x)
+  | |- _ ⊢ (∀ x : _, _) => let x' := fresh x in iIntro (x')
  end.
 Local Tactic Notation "iIntro" :=
  try iStartProof;