diff --git a/tests/proofmode.v b/tests/proofmode.v index d1da557f9775f250826895dafe7ac7957ce1005e..0cc6d3cb030d99e1c51b099a1ef805b3189303dc 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 94359d4b5a9f0fbcbba1362c5cf93f416d9efe2f..c4594b6994149dc83c110564981ca799ff9309d0 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.