From 63311180d51a6849df5257b87ecf5b703480fd06 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 29 Sep 2020 20:19:10 +0200
Subject: [PATCH] Fix broken tests introduced in !522.

---
 tests/proofmode.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tests/proofmode.v b/tests/proofmode.v
index 28d3d010d..fd2bbae5b 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.
-- 
GitLab