diff --git a/tests/proofmode.ref b/tests/proofmode.ref index 393eada0053361382bbf872e1a16a890ad96dc10..7794b340ccd011965e0f47874704ef795daf82a2 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 cee968cb6aa64d44bfaba81f80e7ffa09674b888..941ff8ecbfc758840aece1b81127ff3ca810437c 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 1aebf309ccceff63aaa36f70b1a530d9b497ccdb..5b8f5c49a4d9350a50dc8d4102a537375f498962 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.