From 07ff13e0c8fc3c624b251ef5fba1228a429a6f00 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 15 Jul 2020 14:36:50 +0200
Subject: [PATCH] avoid using iAlways ourselves

---
 tests/proofmode.v         |  4 ++--
 tests/proofmode_monpred.v | 10 +++++-----
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/tests/proofmode.v b/tests/proofmode.v
index f34c1401e..b6a70a421 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -501,7 +501,7 @@ Proof. iIntros "#HPQ HQ !>". iNext. by iRewrite "HPQ" in "HQ". Qed.
 
 Lemma test_iAlways P Q R :
   □ P -∗ <pers> Q → R -∗ <pers> <affine> <affine> P ∗ □ Q.
-Proof. iIntros "#HP #HQ HR". iSplitL. iAlways. done. iAlways. done. Qed.
+Proof. iIntros "#HP #HQ HR". iSplitL. iModIntro. done. iModIntro. done. Qed.
 
 (* A bunch of test cases from #127 to establish that tactics behave the same on
 `⌜ φ ⌝ → P` and `∀ _ : φ, P` *)
@@ -975,7 +975,7 @@ Proof. Fail iStopProof. Abort.
 Check "iAlways_spatial_non_empty".
 Lemma iAlways_spatial_non_empty P :
   P -∗ □ emp.
-Proof. iIntros "HP". Fail iAlways. Abort.
+Proof. iIntros "HP". Fail iModIntro. Abort.
 
 Check "iDestruct_bad_name".
 Lemma iDestruct_bad_name P :
diff --git a/tests/proofmode_monpred.v b/tests/proofmode_monpred.v
index b39d8ab7c..5d7b84d2a 100644
--- a/tests/proofmode_monpred.v
+++ b/tests/proofmode_monpred.v
@@ -71,23 +71,23 @@ Section tests.
   Qed.
 
   Lemma test_objectively P Q : <obj> emp -∗ <obj> P -∗ <obj> Q -∗ <obj> (P ∗ Q).
-  Proof. iIntros "#? HP HQ". iAlways. by iSplitL "HP". Qed.
+  Proof. iIntros "#? HP HQ". iModIntro. by iSplitL "HP". Qed.
 
   Lemma test_objectively_absorbing P Q R `{!Absorbing P} :
     <obj> emp -∗ <obj> P -∗ <obj> Q -∗ R -∗ <obj> (P ∗ Q).
-  Proof. iIntros "#? HP HQ HR". iAlways. by iSplitL "HP". Qed.
+  Proof. iIntros "#? HP HQ HR". iModIntro. by iSplitL "HP". Qed.
 
   Lemma test_objectively_affine P Q R `{!Affine R} :
     <obj> emp -∗ <obj> P -∗ <obj> Q -∗ R -∗ <obj> (P ∗ Q).
-  Proof. iIntros "#? HP HQ HR". iAlways. by iSplitL "HP". Qed.
+  Proof. iIntros "#? HP HQ HR". iModIntro. by iSplitL "HP". Qed.
 
   Lemma test_iModIntro_embed P `{!Affine Q} 𝓟 𝓠 :
     □ P -∗ Q -∗ ⎡𝓟⎤ -∗ ⎡𝓠⎤ -∗ ⎡ 𝓟 ∗ 𝓠 ⎤.
-  Proof. iIntros "#H1 _ H2 H3". iAlways. iFrame. Qed.
+  Proof. iIntros "#H1 _ H2 H3". iModIntro. iFrame. Qed.
 
   Lemma test_iModIntro_embed_objective P `{!Objective Q} 𝓟 𝓠 :
     □ P -∗ Q -∗ ⎡𝓟⎤ -∗ ⎡𝓠⎤ -∗ ⎡ ∀ i, 𝓟 ∗ 𝓠 ∗ Q i ⎤.
-  Proof. iIntros "#H1 H2 H3 H4". iAlways. Show. iFrame. Qed.
+  Proof. iIntros "#H1 H2 H3 H4". iModIntro. Show. iFrame. Qed.
 
   Lemma test_iModIntro_embed_nested P 𝓟 𝓠 :
     □ P -∗ ⎡◇ 𝓟⎤ -∗ ⎡◇ 𝓠⎤ -∗ ⎡ ◇ (𝓟 ∗ 𝓠) ⎤.
-- 
GitLab