From 623c28391b489d75101397e875896f4ee732793e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 11 Apr 2016 23:07:33 +0200
Subject: [PATCH] Fix bug: iIntros "%" was doing the wrong thing.
---
proofmode/tactics.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 6f6c6cc68..0515795d0 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -681,7 +681,7 @@ Tactic Notation "iIntros" constr(pat) :=
| IName ?H :: ?pats => iIntro H; go pats
| IPersistent IAnom :: ?pats => let H := iFresh in iIntro #H; go pats
| IAnom :: ?pats => let H := iFresh in iIntro H; go pats
- | IAnomPure :: ?pats => iPureIntro; go pats
+ | IAnomPure :: ?pats => iIntro {?}; go pats
| IPersistent ?pat :: ?pats =>
let H := iFresh in iIntro #H; iDestructHyp H as pat; go pats
| ?pat :: ?pats =>
--
GitLab