From 5e60826154300c74d0b4bfdc6717cbf4e74f59a5 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 4 Oct 2018 17:41:14 +0200
Subject: [PATCH] fix clear pattern in destruct pattern
---
tests/proofmode.v | 6 ++++++
theories/proofmode/ltac_tactics.v | 10 +++++-----
2 files changed, 11 insertions(+), 5 deletions(-)
diff --git a/tests/proofmode.v b/tests/proofmode.v
index d1da557f9..0cc6d3cb0 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -587,6 +587,12 @@ Proof.
iIntros "?". iExists _. iApply modal_if_lemma2. done.
Qed.
+Lemma test_iDestruct_clear P Q R :
+ P -∗ (Q ∗ R) -∗ True.
+Proof.
+ iIntros "HP HQR". iDestruct "HQR" as "{HP} [HQ HR]". done.
+Qed.
+
End tests.
(** Test specifically if certain things print correctly. *)
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 94359d4b5..c4594b699 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -1102,19 +1102,19 @@ Local Ltac iDestructHypGo Hz pat :=
| IModalElim ?pat => iModCore Hz; iDestructHypGo Hz pat
| _ => fail "iDestruct:" pat "invalid"
end.
-Local Ltac iDestructHypFindPat H pat found pats :=
+Local Ltac iDestructHypFindPat Hgo pat found pats :=
lazymatch pats with
| [] =>
lazymatch found with
| true => pm_prettify (* post-tactic prettification *)
| false => fail "iDestruct:" pat "should contain exactly one proper introduction pattern"
end
- | ISimpl :: ?pats => simpl; iDestructHypFindPat H pat found pats
- | IClear ?H :: ?pats => iClear H; iDestructHypFindPat H pat found pats
- | IClearFrame ?H :: ?pats => iFrame H; iDestructHypFindPat H pat found pats
+ | ISimpl :: ?pats => simpl; iDestructHypFindPat Hgo pat found pats
+ | IClear ?H :: ?pats => iClear H; iDestructHypFindPat Hgo pat found pats
+ | IClearFrame ?H :: ?pats => iFrame H; iDestructHypFindPat Hgo pat found pats
| ?pat :: ?pats =>
lazymatch found with
- | false => iDestructHypGo H pat; iDestructHypFindPat H pat true pats
+ | false => iDestructHypGo Hgo pat; iDestructHypFindPat Hgo pat true pats
| true => fail "iDestruct:" pat "should contain exactly one proper introduction pattern"
end
end.
--
GitLab