From 84144f00df08ad14c5b29c2c7ae74f78b3f07b28 Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Thu, 24 Sep 2020 15:17:18 -0500
Subject: [PATCH] Fix error when destructing as multiple pats
`iDestruct H as "H1 H2"` produces an error that says the pattern should
contain exactly one proper introduction pattern. When multiple patterns
are provided, due to Ltac variable shadowing iDestructHypFindPat was
instead reporting only the first pattern in the error message (and even
that was printed as the parsed AST rather than the original string).
---
tests/proofmode.ref | 3 +++
tests/proofmode.v | 7 ++++++-
theories/proofmode/ltac_tactics.v | 4 ++--
3 files changed, 11 insertions(+), 3 deletions(-)
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 393eada00..7794b340c 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -636,6 +636,9 @@ should contain exactly one proper introduction pattern.
The command has indeed failed with message:
Tactic failure: iDestruct: (IList [[IClear (sel_patterns.SelIdent "HP")]])
invalid.
+The command has indeed failed with message:
+Tactic failure: iDestruct: "HP HQ HR"
+should contain exactly one proper introduction pattern.
"iOrDestruct_fail"
: string
The command has indeed failed with message:
diff --git a/tests/proofmode.v b/tests/proofmode.v
index cee968cb6..941ff8ecb 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1217,7 +1217,12 @@ Proof. Fail iRevert "H". Abort.
Check "iDestruct_fail".
Lemma iDestruct_fail P : P -∗ <absorb> P.
-Proof. iIntros "HP". Fail iDestruct "HP" as "{HP}". Fail iDestruct "HP" as "[{HP}]". Abort.
+Proof.
+ iIntros "HP".
+ Fail iDestruct "HP" as "{HP}".
+ Fail iDestruct "HP" as "[{HP}]".
+ Fail iDestruct "HP" as "HP HQ HR".
+Abort.
Check "iOrDestruct_fail".
Lemma iOrDestruct_fail P : (P ∨ P) -∗ P -∗ P.
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 1aebf309c..5b8f5c49a 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -1453,9 +1453,9 @@ Local Ltac iDestructHypFindPat Hgo 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 =>
+ | ?pat1 :: ?pats =>
lazymatch found with
- | false => iDestructHypGo Hgo pat; iDestructHypFindPat Hgo pat true pats
+ | false => iDestructHypGo Hgo pat1; iDestructHypFindPat Hgo pat true pats
| true => fail "iDestruct:" pat "should contain exactly one proper introduction pattern"
end
end.
--
GitLab