From bfdd67a736ad91c3838bffde3f57af516dec56d8 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 27 Sep 2017 22:31:12 +0200
Subject: [PATCH] Fix `iIntros` regression caused by b0ae1102.
---
theories/proofmode/tactics.v | 2 +-
theories/tests/proofmode.v | 4 ++++
2 files changed, 5 insertions(+), 1 deletion(-)
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 4c7069ccb..2983b97c1 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -939,7 +939,7 @@ Tactic Notation "iIntros" constr(pat) :=
| ?pat :: ?pats =>
let H := iFresh in iIntro H; iDestructHyp H as pat; go pats
end
- in let pats := intro_pat.parse pat in iStartProof; go pats.
+ in let pats := intro_pat.parse pat in try iStartProof; go pats.
Tactic Notation "iIntros" := iIntros [IAll].
Tactic Notation "iIntros" "(" simple_intropattern(x1) ")" :=
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 356a64bd2..c9afe2d6e 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -93,6 +93,10 @@ Proof.
iIntros "# _ //".
Qed.
+Lemma test_very_fast_iIntros P :
+ ∀ x y : nat, ⌜ x = y ⌠-∗ P -∗ P.
+Proof. by iIntros. Qed.
+
Lemma test_iDestruct_spatial_and P Q1 Q2 : P ∗ (Q1 ∧ Q2) -∗ P ∗ Q1.
Proof. iIntros "[H1 [H2 _]]". by iFrame. Qed.
--
GitLab