From acd32497684b1ff5bdcd7baba6b59d42375f61ce Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 18 Feb 2020 21:19:49 +0100
Subject: [PATCH] Stop using deprecated `iAlways` tactic.

---
 theories/base_logic/lib/boxes.v         | 4 ++--
 theories/base_logic/lib/na_invariants.v | 2 +-
 theories/bi/lib/core.v                  | 2 +-
 theories/heap_lang/lib/increment.v      | 2 +-
 theories/proofmode/ltac_tactics.v       | 8 ++++----
 5 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index 2d499a2ed..0205c03a3 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -251,11 +251,11 @@ Proof.
     iDestruct ("HQQ'" with "HQ") as "HQ'".
     iMod (slice_insert_full with "HQ' Hb") as (γ' ?) "[#Hs' Hb]"; try done.
     iExists γ', _. iIntros "{$∗ $# $%} !>". do 2 iNext. iRewrite "Heq".
-    iAlways. by iSplit; iIntros "[? $]"; iApply "HQQ'".
+    iIntros "!>". by iSplit; iIntros "[? $]"; iApply "HQQ'".
   - iMod (slice_delete_empty with "Hs Hb") as (P') "(Heq & Hb)"; try done.
     iMod (slice_insert_empty with "Hb") as (γ' ?) "[#Hs' Hb]"; try done.
     iExists γ', (Q' ∗ P')%I. iIntros "{$∗ $# $%} !>".  do 2 iNext. iRewrite "Heq".
-    iAlways. by iSplit; iIntros "[? $]"; iApply "HQQ'".
+    iIntros "!>". by iSplit; iIntros "[? $]"; iApply "HQQ'".
 Qed.
 
 Lemma slice_split E q f P Q1 Q2 γ b :
diff --git a/theories/base_logic/lib/na_invariants.v b/theories/base_logic/lib/na_invariants.v
index 40b9d0671..8ce782b03 100644
--- a/theories/base_logic/lib/na_invariants.v
+++ b/theories/base_logic/lib/na_invariants.v
@@ -47,7 +47,7 @@ Section proofs.
   Proof.
     iIntros "#HPQ". rewrite /na_inv. iDestruct 1 as (i ?) "#Hinv".
     iExists i. iSplit; first done. iApply (inv_iff with "[] Hinv").
-    iNext; iAlways.
+    iIntros "!> !>".
     iSplit; iIntros "[[? Ho]|$]"; iLeft; iFrame "Ho"; by iApply "HPQ".
   Qed.
 
diff --git a/theories/bi/lib/core.v b/theories/bi/lib/core.v
index 2d737e655..a0316b83a 100644
--- a/theories/bi/lib/core.v
+++ b/theories/bi/lib/core.v
@@ -50,7 +50,7 @@ Section core.
   Proof.
     split.
     - iIntros (HP) "HP". iDestruct (coreP_intro with "HP") as "#HcP".
-      iAlways. by iApply HP.
+      iIntros "!>". by iApply HP.
     - iIntros (HPQ) "HcP". iDestruct (coreP_mono _ _ HPQ with "HcP") as "HcQ".
       by iDestruct (coreP_elim with "HcQ") as "#HQ".
   Qed.
diff --git a/theories/heap_lang/lib/increment.v b/theories/heap_lang/lib/increment.v
index ef86e1aef..265570c95 100644
--- a/theories/heap_lang/lib/increment.v
+++ b/theories/heap_lang/lib/increment.v
@@ -149,7 +149,7 @@ Section increment_client.
     (* FIXME: I am only using persistent stuff, so I should be allowed
        to move this to the persisten context even without the additional â–¡. *)
     iAssert (â–¡ WP incr #l {{ _, True }})%I as "#Aupd".
-    { iAlways. awp_apply incr_spec. clear x.
+    { iIntros "!>". awp_apply incr_spec. clear x.
       iInv nroot as (x) ">H↦". iAaccIntro with "H↦"; first by eauto 10.
       iIntros "H↦ !>". iSplitL "H↦"; first by eauto 10.
       (* The continuation: From after the atomic triple to the postcondition of the WP *)
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index e01b36782..bf120ccd7 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -3218,10 +3218,10 @@ Hint Extern 1 (envs_entails _ (_ ∧ _)) => iSplit : core.
 Hint Extern 1 (envs_entails _ (_ ∗ _)) => iSplit : core.
 Hint Extern 1 (envs_entails _ (_ ∗-∗ _)) => iSplit : core.
 Hint Extern 1 (envs_entails _ (â–· _)) => iNext : core.
-Hint Extern 1 (envs_entails _ (â–  _)) => iAlways : core.
-Hint Extern 1 (envs_entails _ (<pers> _)) => iAlways : core.
-Hint Extern 1 (envs_entails _ (<affine> _)) => iAlways : core.
-Hint Extern 1 (envs_entails _ (â–¡ _)) => iAlways : core.
+Hint Extern 1 (envs_entails _ (â–  _)) => iModIntro : core.
+Hint Extern 1 (envs_entails _ (<pers> _)) => iModIntro : core.
+Hint Extern 1 (envs_entails _ (<affine> _)) => iModIntro : core.
+Hint Extern 1 (envs_entails _ (â–¡ _)) => iModIntro : core.
 Hint Extern 1 (envs_entails _ (∃ _, _)) => iExists _ : core.
 Hint Extern 1 (envs_entails _ (∃.. _, _)) => iExists _ : core.
 Hint Extern 1 (envs_entails _ (â—‡ _)) => iModIntro : core.
-- 
GitLab