diff --git a/tests/proofmode.v b/tests/proofmode.v index 28d3d010d1c9c466b54035267e9b0325ef421f63..fd2bbae5b13a7dc40e615956f143a5c40091c644 100644 --- a/tests/proofmode.v +++ b/tests/proofmode.v @@ -457,10 +457,10 @@ Proof. iIntros "H1 H2". by iFrame "H1". Qed. Lemma test_iFrame_affinely_1 P Q `{!Affine P} : P -∗ <affine> Q -∗ <affine> (P ∗ Q). -Proof. iIntros "HP HQ". iFrame "HQ". iExact "HP". Qed. +Proof. iIntros "HP HQ". iFrame "HQ". by iModIntro. Qed. Lemma test_iFrame_affinely_2 P Q `{!Affine P, !Affine Q} : P -∗ Q -∗ <affine> (P ∗ Q). -Proof. iIntros "HP HQ". iFrame "HQ". iExact "HP". Qed. +Proof. iIntros "HP HQ". iFrame "HQ". by iModIntro. Qed. Lemma test_iAssert_modality P : ◇ False -∗ ▷ P. Proof.