diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index 2d499a2edb494fabd23893c9751742e61cf6b48b..0205c03a397a6d45dfed2c42339156610151e9bb 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 40b9d06712268ede97b35eb8deeec4e7dbffafed..8ce782b03950dbd1db90c523128a9c35af9ec70f 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 2d737e6554685c4baaa30c7805e27a272d0dc1d9..a0316b83af011f838eafc218f675149eca8e48ef 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 ef86e1aef8595ee6c042c5aaf36b5a402d0833fc..265570c95f2df48c5a94a0f291a5c9c8d3a7f262 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 e01b3678292ed6247d4b42e1145b2ef8deefd5ab..bf120ccd7c8c9e5cf1804eb03b4cffd6daf57050 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.