diff --git a/tests/proofmode.v b/tests/proofmode.v index 31cc46faa14e1b1d2bf74238b14435a34b6fd889..7b2ac9d6b43f5e839bc98a4a6fe94f0386b0139f 100644 --- a/tests/proofmode.v +++ b/tests/proofmode.v @@ -1633,4 +1633,21 @@ Proof. iFrame select _. Qed. +Lemma test_iDestruct_split_reuse_name P Q : + P ∗ Q -∗ P ∗ Q. +Proof. + iIntros "H". + iDestruct "H" as "[? H]". Undo. + iDestruct "H" as "[H ?]". Undo. + auto. +Qed. + +Lemma test_iDestruct_split_reuse_name_2 P Q R : + (P ∗ Q) ∗ R -∗ (P ∗ Q) ∗ R. +Proof. + iIntros "H". + iDestruct "H" as "[[H H'] ?]". Undo. + auto. +Qed. + End tactic_tests.