diff --git a/opam b/opam
index 910aadf30407559c6906071a6be47a0af16703b5..1d9bf8ecd1a2865f488966ee039ec124e81dd604 100644
--- a/opam
+++ b/opam
@@ -16,7 +16,7 @@ This branch uses a proper weak memory model.
 """
 
 depends: [
-  "coq-gpfsl" { (= "dev.2020-07-15.0.654300d3") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2020-07-22.1.6569264a") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lang/lock.v b/theories/lang/lock.v
index 5c7ad23065f54ffb494d1ab6c3767dfa7e5d10c2..b3076cfc543c54b48c0d755bb77b10c965b70953 100644
--- a/theories/lang/lock.v
+++ b/theories/lang/lock.v
@@ -67,7 +67,7 @@ Section proof.
   Proof.
     iIntros "#HR !#".
     iSplit; iIntros "Hlck"; iApply (lock_proto_iff with "[HR] Hlck"); [done|].
-    iAlways; iSplit; iIntros; by iApply "HR".
+    iModIntro; iSplit; iIntros; by iApply "HR".
   Qed.
 
   Lemma lock_interp_comparable l γ t s v R:
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index e4c6fb340fae4f8f895a2a24328304b5758c355b..59a4ce454092d8d7dc9233f97a27af592b97b482 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -55,7 +55,7 @@ Section frac_bor.
     ▷ □ (∀ q, φ q ↔ φ' q) -∗ &frac{κ}φ -∗ &frac{κ}φ'.
   Proof.
     iIntros "#Hφφ' H". iDestruct "H" as (γ κ' V0 φ0) "(? & ? & #Hφ0φ & ?)".
-    iExists γ, κ', V0, φ0. iFrame. iNext. iAlways. iIntros (q).
+    iExists γ, κ', V0, φ0. iFrame. iNext. iModIntro. iIntros (q).
     iSplit; iIntros "H".
     - iApply "Hφφ'". by iApply "Hφ0φ".
     - iApply "Hφ0φ". by iApply "Hφφ'".
@@ -74,7 +74,7 @@ Section frac_bor.
       iMod ("Hclose" with "[] [-]") as "Hφ"; last first.
       { iExists γ, κ', V, φ. iFrame "#". iSplitR; [|iSplitR].
         - iIntros "!>!>!#*". by iApply (bi.iff_refl True%I).
-        - iModIntro. iNext. iAlways. iIntros (??).
+        - iModIntro. iNext. iModIntro. iIntros (??).
           rewrite !bi.intuitionistically_elim. iApply ("Hfrac'" $! _ _).
         - by iApply (in_at_bor_share with "[Hφ]"). }
       { iNext. iSplit. iDestruct "Hφ" as "[$ _]". iExists 1%Qp, 0, 0.
@@ -96,7 +96,7 @@ Section frac_bor.
       iDestruct "H" as (κ') "(#? & #? & >_)". iExists γ, κ', V, φ. iFrame "#".
       iSplitR; [|iSplitR].
       + iIntros "!> !> !# *". by iApply (bi.iff_refl True%I).
-      + iModIntro. iNext. iAlways. iIntros (??).
+      + iModIntro. iNext. iModIntro. iIntros (??).
         rewrite !bi.intuitionistically_elim. iApply ("Hfrac'" $! _ _).
       + by iApply in_at_bor_fake.
   Qed.
@@ -217,7 +217,7 @@ Section frac_bor.
   Lemma frac_bor_lft_incl `{LatBottom Lat} κ κ' q:
     ⎡lft_ctx⎤ -∗ &frac{κ}(λ q', (q * q').[κ']) -∗ κ ⊑ κ'.
   Proof.
-    iIntros "#LFT#Hbor". iApply lft_incl_intro. iAlways. iIntros (q') "Hκ'".
+    iIntros "#LFT#Hbor". iApply lft_incl_intro. iModIntro. iIntros (q') "Hκ'".
     iMod (frac_bor_acc with "LFT Hbor Hκ'") as (q'') "[>Htok Hclose]". done.
     iExists _. iIntros "{$Htok} !> Hκ'". by iApply "Hclose".
   Qed.
diff --git a/theories/lifetime/model/borrow_sep.v b/theories/lifetime/model/borrow_sep.v
index a3fcd0ea479cef14eafb6469ef5c2ff1d3f02e5d..fdfbddf59d9f46a4d56af11a3c4badfc10107abd 100644
--- a/theories/lifetime/model/borrow_sep.v
+++ b/theories/lifetime/model/borrow_sep.v
@@ -91,11 +91,11 @@ Proof.
   rewrite !own_bor_op. iDestruct "Hbor" as "[[H● H◯Q] H◯P]".
   iAssert (&{κ}P)%I with "[H◯P]" as "$".
   { rewrite /bor /raw_bor /idx_bor_own /=. iExists κ'. iFrame "Hκκ'". iExists γP.
-    iSplitL; [by auto with iFrame|]. iExists _. iFrame "#". iNext. iAlways.
+    iSplitL; [by auto with iFrame|]. iExists _. iFrame "#". iNext. iModIntro.
     iSplit; [|by auto]. iIntros "[_ H]". by iApply "H". }
   iAssert (&{κ}Q)%I with "[H◯Q]" as "$".
   { rewrite /bor /raw_bor /idx_bor_own /=. iExists κ'. iFrame "Hκκ'". iExists γQ.
-    iSplitL; [by auto with iFrame|]. iExists _. iFrame "#". iNext. iAlways.
+    iSplitL; [by auto with iFrame|]. iExists _. iFrame "#". iNext. iModIntro.
     iSplit; [|by auto]. iIntros "[_ H]". by iApply "H". }
   iMod ("Hclose" with "[-]"); [|done]. iModIntro ⎡_⎤%I. iExists A, I. iFrame.
   rewrite big_sepS_later. iApply "Hclose'". iExists Vκ. iSplit; [done|].
@@ -179,7 +179,7 @@ Proof.
     - iExists _. simpl. iFrame. iCombine "HV1 HV2" as "HV12".
       iDestruct (monPred_in_intro with "HV12") as (V12) "(HV12' & % & %)".
       iApply (monPred_in_elim _ V12). done. rewrite monPred_at_in. solve_lat.
-    - iExists _. iFrame. iNext. iAlways.
+    - iExists _. iFrame. iNext. iModIntro.
       by iSplit; iIntros "[HP HQ]"; iSplitL "HP"; (iApply "HPP'" || iApply "HQQ'"). }
   iMod ("Hclose" with "[-]"); [|done]. iExists A, I. iFrame. rewrite big_sepS_later.
   iApply "Hclose'". iExists _. iSplit; [done|]. iLeft. iSplit; [|done].
diff --git a/theories/lifetime/model/boxes.v b/theories/lifetime/model/boxes.v
index 7d42ddc2ed631d1777dc1dee34c9a0db0e431159..772c9b7cc9f0385be4d2e95c7bf8b6107afba039 100644
--- a/theories/lifetime/model/boxes.v
+++ b/theories/lifetime/model/boxes.v
@@ -220,7 +220,7 @@ Proof.
   iCombine "Hf" "HP'" as "Hf".
   rewrite -big_sepM_sep big_sepM_fmap; iApply (big_sepM_fupd _ _ f).
   iApply (@big_sepM_impl with "[$Hf]").
-  iAlways; iIntros (γ b' ?) "[(Hγ' & #$ & #$) HΦ]".
+  iModIntro; iIntros (γ b' ?) "[(Hγ' & #$ & #$) HΦ]".
   iInv N as (b) "[>Hγ _]" "Hclose".
   iMod (box_own_auth_update γ with "[Hγ Hγ']") as "[Hγ $]"; first by iFrame.
   iApply "Hclose". iNext; iExists (Some $ to_latT V). by iFrame.
@@ -236,7 +236,7 @@ Proof.
     [∗ map] γ↦b ∈ f, box_own_auth γ (◯ Excl' None) ∗  box_own_prop γ (Φ γ) ∗
       inv N (slice_inv γ (Φ γ)))%I with "[> Hf]" as "[HΦ ?]".
   { rewrite -big_sepM_sep -big_sepM_fupd. iApply (@big_sepM_impl with "[$Hf]").
-    iAlways; iIntros (γ o ?) "(Hγ' & #HγΦ & #Hinv)".
+    iModIntro; iIntros (γ o ?) "(Hγ' & #HγΦ & #Hinv)".
     assert (Ho : from_option (.⊑ V) False o) by eauto.
     destruct o as [V'|]=>//. rewrite -Ho.
     iInv N as (b) "[>Hγ HΦ]" "Hclose".
@@ -261,11 +261,11 @@ Proof.
   - iMod (slice_delete_full with "Hs Hb") as (P') "(HQ & #Heq & Hb)"; try done.
     iDestruct ("HQQ'" with "HQ") as "HQ'".
     iMod (slice_insert_full with "HQ' Hb") as (γ') "(% & #Hs' & Hb)"; try done.
-    iExists γ', _. iFrame "∗#%". iIntros "!>". do 2 iNext. iAlways. iIntros (V).
+    iExists γ', _. iFrame "∗#%". iIntros "!>". do 2 iNext. iModIntro. iIntros (V).
     iRewrite "Heq". by iSplit; iIntros "[? $]"; iApply "HQQ'".
   - iDestruct (slice_delete_empty with "Hs Hb") as (P') "(#Heq & Hb)"; [done|].
     iMod (slice_insert_empty with "Hb") as (γ') "(% & #Hs' & Hb)"; try done.
-    iExists γ', _. iFrame "∗#%". iIntros "!>". do 2 iNext. iAlways. iIntros (V).
+    iExists γ', _. iFrame "∗#%". iIntros "!>". do 2 iNext. iModIntro. iIntros (V).
     iRewrite "Heq". by iSplit; iIntros "[? $]"; iApply "HQQ'".
 Qed.
 
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index 6e71e3e083f62898200ac8f005c5b74b4fbcb774..c3525888f46f3b07ef4ceb5c43e95f505393412a 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -71,7 +71,7 @@ Proof.
   pose (Kalive := filter (lft_alive_in A) K).
   destruct (decide (Kalive = ∅)) as [HKalive|].
   { iModIntro. rewrite /Iinv. iFrame.
-    iApply (@big_sepS_impl with "[$HK]"); iAlways.
+    iApply (@big_sepS_impl with "[$HK]"); iModIntro.
     iIntros (κ Hκ) "[(_ & _ & %)|[$ _]]". set_solver. }
   destruct (minimal_exists_L (⊂) Kalive)
     as (κ & [Hκalive HκK]%elem_of_filter & Hκmin); first done.
@@ -146,7 +146,7 @@ Proof.
     + apply Hmono=>//; rewrite elem_of_difference elem_of_singleton; auto.
   - rewrite (big_sepS_delete _ K) //. iSplitL "Hinv".
     + by rewrite functions.fn_lookup_insert -lat_join_sqsubseteq_l.
-    + iApply (@big_sepS_impl with "[$HK]"). iAlways. iIntros (κ').
+    + iApply (@big_sepS_impl with "[$HK]"). iModIntro. iIntros (κ').
       rewrite elem_of_difference elem_of_singleton. iIntros ([??]) "H".
         rewrite functions.fn_lookup_insert_ne //.
 Qed.
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 1d98bb66c8e2c44783b02fadd74a30dc52ad10ec..bcda1f20c066dcb3d1a0e2ecf3dc19b65d71e835 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -397,14 +397,14 @@ Lemma raw_bor_iff i P P' :
 Proof.
   iIntros "#HPP' HP". unfold raw_bor. iDestruct "HP" as (s) "[HiP HP]".
   iExists s. iFrame. iDestruct "HP" as (P0) "[#Hiff ?]". iExists P0. iFrame.
-  iNext. iAlways. iSplit; iIntros.
+  iNext. iModIntro. iSplit; iIntros.
     by iApply "HPP'"; iApply "Hiff". by iApply "Hiff"; iApply "HPP'".
 Qed.
 
 Lemma idx_bor_iff κ i P P' : ▷ □ (P ↔ P') -∗ &{κ,i}P -∗ &{κ,i}P'.
 Proof.
   unfold idx_bor. iIntros "#HPP' [$ HP]". iDestruct "HP" as (P0) "[#HP0P Hs]".
-  iExists P0. iFrame. iNext. iAlways. iSplit; iIntros.
+  iExists P0. iFrame. iNext. iModIntro. iSplit; iIntros.
     by iApply "HPP'"; iApply "HP0P". by iApply "HP0P"; iApply "HPP'".
 Qed.
 
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 588011929b29a7c50efab5996f5401f8f727b00f..802638e602533a64cc01978e7d746c17b127492c 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -281,7 +281,7 @@ Section typing.
       + iApply "HE'". iIntros "{$# Hf Hinh HE' LFT HE %}".
         iInduction κs as [|κ κs] "IH"=> //=. iSplitL.
         { iApply lft_incl_trans; first done. iApply lft_intersect_incl_l. }
-        iApply "IH". iAlways. iApply lft_incl_trans; first done.
+        iApply "IH". iModIntro. iApply lft_incl_trans; first done.
         iApply lft_intersect_incl_r.
       + iSplitL; last done. iExists ϝ. iSplit; first by rewrite /= left_id.
         iFrame "#∗".
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index c4335c6b99cbf32f779089bdefb6a94ba81e4a1f..94937ba4e3f775aadd41fb1dd72511cc04733a10 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -212,7 +212,7 @@ Section arc.
   Next Obligation.
     iIntros (ty κ κ' tid l) "#Hincl H". iDestruct "H" as (l') "[#Hl #Hshr]".
     iExists _. iSplit; first by iApply frac_bor_shorten.
-    iAlways. iIntros (F q) "% Htok".
+    iModIntro. iIntros (F q) "% Htok".
     iMod (lft_incl_acc with "Hincl Htok") as (q'') "[Htok Hclose]"; first solve_ndisj.
     iMod ("Hshr" with "[] Htok") as "Hshr2"; first done.
     iModIntro. iNext. iMod "Hshr2" as "[Htok HX]".
@@ -239,7 +239,7 @@ Section arc.
     type_incl ty1 ty2 -∗ type_incl (arc ty1) (arc ty2).
   Proof.
     iIntros "#Hincl". iPoseProof "Hincl" as "(#Hsz & #Hoincl & #Hsincl)".
-    iSplit; first done. iSplit; iAlways.
+    iSplit; first done. iSplit; iModIntro.
     - iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
       iDestruct "Hvl" as "[(Hl1 & Hl2 & H† & Hc) | Hvl]".
       { iLeft. iFrame. iDestruct "Hsz" as %->.
@@ -338,7 +338,7 @@ Section arc.
   Next Obligation.
     iIntros (ty κ κ' tid l) "#Hincl H". iDestruct "H" as (l') "[#Hl #Hshr]".
     iExists _. iSplit; first by iApply frac_bor_shorten.
-    iAlways. iIntros (F q) "% Htok".
+    iModIntro. iIntros (F q) "% Htok".
     iMod (lft_incl_acc with "Hincl Htok") as (q'') "[Htok Hclose]"; first solve_ndisj.
     iMod ("Hshr" with "[] Htok") as "Hshr2"; first done.
     iModIntro. iNext. iMod "Hshr2" as "[Htok HX]".
@@ -364,7 +364,7 @@ Section arc.
     type_incl ty1 ty2 -∗ type_incl (weak ty1) (weak ty2).
   Proof.
     iIntros "#Hincl". iPoseProof "Hincl" as "(#Hsz & #Hoincl & #Hsincl)".
-    iSplit; first done. iSplit; iAlways.
+    iSplit; first done. iSplit; iModIntro.
     - iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
       iDestruct "Hvl" as (???? ν ? ?) "(#Hpersist & Htk)".
       iExists _, _, _, _, _, _, _. iFrame "#∗". by iApply arc_persist_type_incl.
@@ -884,9 +884,9 @@ Section arc.
       { iIntros "_". wp_if. unlock. iFrame. iExists (_::_). rewrite heap_mapsto_vec_cons.
         iFrame. iExists 1%nat, _, []. rewrite /= right_id_L Max.max_0_r.
         auto 10 with iFrame. }
-      iIntros "([H† H1] & H2 & H3)". iDestruct "H1" as (vl') "[H1 Heq]".
+      iIntros "([H† H1] & H2 & H3)". iDestruct "H1" as (vl1) "[H1 Heq]".
       iDestruct "Heq" as %<-. wp_if.
-      wp_apply (wp_delete _ _ _ _ (_::_::vl') with "[H1 H2 H3 H†]"); [done|..].
+      wp_apply (wp_delete _ _ _ _ (_::_::vl1) with "[H1 H2 H3 H†]"); [done|..].
       { simpl. lia. }
       { rewrite 2!heap_mapsto_vec_cons shift_loc_assoc. auto with iFrame. }
       iFrame. iIntros "_". iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame.
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index 352f6dc95edacd556bbd9ed3607283186b4494ef..263bd1faa6868be6fe832da01489c8272011a5ad 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -39,7 +39,7 @@ Section cell.
     iDestruct ("EQ" with "HE") as "(% & #Hown & #Hshr)".
     iSplit; [done|iSplit; iIntros "!# * H"].
     - iApply ("Hown" with "H").
-    - iApply na_bor_iff; last done. iNext; iAlways; iSplit; iIntros "H";
+    - iApply na_bor_iff; last done. iNext; iModIntro; iSplit; iIntros "H";
       iDestruct "H" as (vl) "[??]"; iExists vl; iFrame; by iApply "Hown".
   Qed.
   Lemma cell_mono' E L ty1 ty2 : eqtype E L ty1 ty2 → subtype E L (cell ty1) (cell ty2).
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index 64a0971483e72d5e8b8088a49ad49f1abcb18a44..b82ba926e2a6bb4382e4ff7364eb666977471840 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -95,7 +95,7 @@ Section mutex.
       iExists γ.
       iApply lock_proto_iff_proper; [|iFrame].
       iApply bor_iff_proper. iApply heap_mapsto_pred_iff_proper.
-      iNext. iAlways; iIntros; iSplit; iIntros; by iApply "Howni".
+      iNext. iModIntro; iIntros; iSplit; iIntros; by iApply "Howni".
   Qed.
 
   Global Instance mutex_proper E L :
@@ -116,7 +116,7 @@ Section mutex.
     iExists _. iFrame "Hincl". iDestruct "Hshr" as (γ) "Hproto".
     iExists γ. iApply lock_proto_iff_proper; [|iFrame].
     iApply bor_iff_proper. iApply heap_mapsto_pred_iff_proper.
-    iNext. iAlways; iIntros; iSplit; iIntros; by iApply send_change_tid.
+    iNext. iModIntro; iIntros; iSplit; iIntros; by iApply send_change_tid.
   Qed.
 End mutex.
 
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index 28f36d795e25e7055f55630a78ebbb5712bd2345..de85d02cebdb992db14f69cfebcf3b4a4fe5463e 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -89,7 +89,7 @@ Section mguard.
     intros α1 α2 Hα ty1 ty2 Hty. generalize Hty. rewrite eqtype_unfold. iIntros (Hty' q) "HL".
     iDestruct (Hty' with "HL") as "#Hty". clear Hty'. iDestruct (Hα with "HL") as "#Hα".
     iIntros "!# #HE". iDestruct ("Hα" with "HE") as "{Hα} Hα".
-    iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs) {HE Hty}". iSplit; [done|iSplit; iAlways].
+    iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs) {HE Hty}". iSplit; [done|iSplit; iModIntro].
     - iIntros (tid [|[[]|][]]) "H"; try done. simpl.
       iDestruct "H" as (β) "(#H⊑ & Hinv & Hown)".
       iExists β. iFrame. iSplit; last iSplit.
@@ -98,10 +98,10 @@ Section mguard.
         iExists γ. iApply (lock_proto_lft_mono with "Hα").
         iApply lock_proto_iff_proper; [|iFrame].
         iApply bor_iff_proper. iNext. iApply heap_mapsto_pred_iff_proper.
-        iAlways; iIntros; iSplit; iIntros; by iApply "Ho".
+        iModIntro; iIntros; iSplit; iIntros; by iApply "Ho".
       + iApply bor_iff; last done. iIntros "!>".
         iApply heap_mapsto_pred_iff_proper.
-        iAlways; iIntros; iSplit; iIntros; by iApply "Ho".
+        iModIntro; iIntros; iSplit; iIntros; by iApply "Ho".
     - iIntros (κ tid l) "H". iDestruct "H" as (l') "H". iExists l'.
       iDestruct "H" as "[$ #H]". iIntros "!# * % Htok".
       iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index e1f93314cb698e1ae0e8585b5acd52ca7fc1db28..a50131a61ea65bd21dadd6fbba186a29eb14eed0 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -191,7 +191,7 @@ Section rc.
   Next Obligation.
     iIntros (ty κ κ' tid l) "#Hincl H". iDestruct "H" as (l') "[#Hl #Hshr]".
     iExists _. iSplit; first by iApply frac_bor_shorten.
-    iAlways. iIntros (F q) "% Htok".
+    iModIntro. iIntros (F q) "% Htok".
     iMod (lft_incl_acc with "Hincl Htok") as (q'') "[Htok Hclose]"; first solve_ndisj.
     iMod ("Hshr" with "[] Htok") as "Hshr2"; first done.
     iModIntro. iNext. iMod "Hshr2" as "[Htok HX]".
@@ -218,7 +218,7 @@ Section rc.
     type_incl ty1 ty2 -∗ type_incl (rc ty1) (rc ty2).
   Proof.
     iIntros "#Hincl". iPoseProof "Hincl" as "(#Hsz & #Hoincl & #Hsincl)".
-    iSplit; first done. iSplit; iAlways.
+    iSplit; first done. iSplit; iModIntro.
     - iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
       iDestruct "Hvl" as "[(Hl1 & Hl2 & H† & Hc) | Hvl]".
       { iLeft. iFrame. iDestruct "Hsz" as %->.
@@ -691,7 +691,7 @@ Section code.
     iApply (type_cont [] [ϝ ⊑ₗ []]
                       (λ _, [rcx ◁ box (uninit 1); r ◁ box (Σ[ ty; rc ty ])])) ;
       [solve_typing..| |]; last first.
-    { simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
+    { simpl. iModIntro. iIntros (k arg). inv_vec arg. simpl_subst.
       iApply type_delete; [solve_typing..|].
       iApply type_jump; solve_typing. }
     iIntros (k). simpl_subst.
@@ -786,7 +786,7 @@ Section code.
     iApply (type_cont [] [ϝ ⊑ₗ []]
                       (λ _, [rcx ◁ box (uninit 1); r ◁ box (option ty)]));
       [solve_typing..| |]; last first.
-    { simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
+    { simpl. iModIntro. iIntros (k arg). inv_vec arg. simpl_subst.
       iApply type_delete; [solve_typing..|].
       iApply type_jump; solve_typing. }
     iIntros (k). simpl_subst.
@@ -876,7 +876,7 @@ Section code.
     iApply (type_cont [] [ϝ ⊑ₗ []]
                       (λ _, [rcx ◁ box (uninit 1); r ◁ box (option $ &uniq{α}ty)]));
       [solve_typing..| |]; last first.
-    { simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
+    { simpl. iModIntro. iIntros (k arg). inv_vec arg. simpl_subst.
       iApply type_delete; [solve_typing..|].
       iApply type_jump; solve_typing. }
     iIntros (k). simpl_subst.
@@ -1008,7 +1008,7 @@ Section code.
     iApply (type_cont [] [ϝ ⊑ₗ []]
                       (λ _, [rcx ◁ box (uninit 1); r ◁ box (&uniq{α}ty)]));
       [solve_typing..| |]; last first.
-    { simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
+    { simpl. iModIntro. iIntros (k arg). inv_vec arg. simpl_subst.
       iApply type_delete; [solve_typing..|].
       iApply type_jump; solve_typing. }
     iIntros (k). simpl_subst.
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 7f441063b9ee28cc2c638dd05e65da1bd076f267..798b16c70dfe660ae082e51b8ef8e878537a7dc2 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -63,7 +63,7 @@ Section weak.
   Next Obligation.
     iIntros (ty κ κ' tid l) "#Hincl H". iDestruct "H" as (l') "[#Hl #Hshr]".
     iExists _. iSplit; first by iApply frac_bor_shorten.
-    iAlways. iIntros (F q) "% Htok".
+    iModIntro. iIntros (F q) "% Htok".
     iMod (lft_incl_acc with "Hincl Htok") as (q'') "[Htok Hclose]"; first solve_ndisj.
     iMod ("Hshr" with "[] Htok") as "Hshr2"; first done.
     iModIntro. iNext. iMod "Hshr2" as "[Htok HX]".
@@ -88,7 +88,7 @@ Section weak.
     type_incl ty1 ty2 -∗ type_incl (weak ty1) (weak ty2).
   Proof.
     iIntros "#Hincl". iPoseProof "Hincl" as "(Hsz & #Hoincl & #Hsincl)".
-    iSplit; first done. iSplit; iAlways.
+    iSplit; first done. iSplit; iModIntro.
     - iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
       iDestruct "Hvl" as (γ ν) "(#Hpersist & Htok)".
       iExists _, _. iFrame "Htok". by iApply rc_persist_type_incl.
@@ -138,7 +138,7 @@ Section code.
     iApply (type_cont [] [ϝ ⊑ₗ []]
                       (λ _, [w ◁ box (&shr{α}(weak ty)); r ◁ box (option (rc ty))])) ;
       [solve_typing..| |]; last first.
-    { simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
+    { simpl. iModIntro. iIntros (k arg). inv_vec arg. simpl_subst.
       iApply type_delete; [solve_typing..|].
       iApply type_jump; solve_typing. }
     iIntros (k). simpl_subst.
@@ -386,7 +386,7 @@ Section code.
     iIntros (_ ϝ ret arg). inv_vec arg=>w. simpl_subst.
     iApply (type_cont [] [ϝ ⊑ₗ []] (λ _, [w ◁ box (uninit 1)]));
       [solve_typing..| |]; last first.
-    { simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
+    { simpl. iModIntro. iIntros (k arg). inv_vec arg. simpl_subst.
       iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
       iApply type_delete; [solve_typing..|].
       iApply type_jump; solve_typing. }
diff --git a/theories/typing/lib/refcell/ref.v b/theories/typing/lib/refcell/ref.v
index 321feb64ae5094cef07641ffba6636fefbab8f8f..d24833bfb619038c5a8334d34b68a83a41740260 100644
--- a/theories/typing/lib/refcell/ref.v
+++ b/theories/typing/lib/refcell/ref.v
@@ -82,7 +82,7 @@ Section ref.
     iIntros (α1 α2 Hα ty1 ty2 Hty q) "HL".
     iDestruct (Hty with "HL") as "#Hty". iDestruct (Hα with "HL") as "#Hα".
     iIntros "!# #HE". iDestruct ("Hα" with "HE") as "Hα1α2".
-    iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [|iSplit; iAlways].
+    iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [|iSplit; iModIntro].
     - done.
     - iIntros (tid [|[[]|][|[[]|][]]]) "H"=>//=.
       iDestruct "H" as (ν q' γ β ty') "(#Hshr & #H⊑ & #Hinv & Htok & Hown)".
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 81ac8abd96a065f867295e84f29c7d819dfe6808..c76a26347bf0098658cc965276b2cd8c5736312c 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -316,8 +316,8 @@ Section ref_functions.
     iDestruct ("Hclose3" with "Hαν") as "[Hα Hν]".
     iMod ("Hclose2" with "Hϝ HL") as "HL".
     wp_rec. iDestruct "Hr" as "[Hr Hr†]".
-    iDestruct "Hr" as (?) "[Hr H]". iDestruct "H" as (vl1 ? ->) "[#Hr1' H]".
-    iDestruct "H" as (vl2 ? ->) "[#Hr2' ->]".
+    iDestruct "Hr" as (?) "[Hr H]". iDestruct "H" as (vl1 vl1' ->) "[#Hr1' H]".
+    iDestruct "H" as (vl2 vl2' ->) "[#Hr2' ->]".
     destruct vl1 as [|[[|lr1|]|] []], vl2 as [|[[|lr2|]|] []]=>//=.
     rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
     iDestruct "Hr" as "[Hr1 Hr2]". wp_read. wp_let. wp_op. wp_read. wp_let.
@@ -329,15 +329,15 @@ Section ref_functions.
     iMod (na_bor_acc with "LFT Hinv Hβ Hna") as "(INV & Hna & Hclosena)"; [done..|].
     wp_seq. wp_op. wp_read.
     iDestruct (refcell_inv_reading_inv with "INV Hγ")
-      as (q' n) "(H↦lrc & _ & [H● H◯] & H† & Hq' & Hshr')".
-    iDestruct "Hq'" as (q'') "(Hq'q'' & Hν1 & Hν2)".
-    iDestruct "Hq'q''" as %Hq'q''. iMod (own_update with "H●") as "[H● ?]".
+      as (q1 n) "(H↦lrc & _ & [H● H◯] & H† & Hq1 & Hshr')".
+    iDestruct "Hq1" as (q2) "(Hq1q2 & Hν1 & Hν2)".
+    iDestruct "Hq1q2" as %Hq1q2. iMod (own_update with "H●") as "[H● ?]".
     { apply auth_update_alloc,
-         (op_local_update_discrete _ _ (reading_stR (q''/2)%Qp ν))=>-[Hagv _].
+         (op_local_update_discrete _ _ (reading_stR (q2/2)%Qp ν))=>-[Hagv _].
       split; [split|done].
       - by rewrite /= agree_idemp.
-      - apply frac_valid'. rewrite -Hq'q'' comm -{2}(Qp_div_2 q'').
-        apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q''/2)%Qp).
+      - apply frac_valid'. rewrite -Hq1q2 comm -{2}(Qp_div_2 q2).
+        apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q2/2)%Qp).
         apply Qcplus_le_mono_r, Qp_ge_0. }
     wp_let. wp_read. wp_let. wp_op. wp_write.
     wp_apply (wp_delete _ _ _ _ [_; _] with "[Href↦1 Href↦2 Href†]")=>//.
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index ec39aa1fdba40521280aa418e0d79428b9a3dfc2..9885374161d181da3ceac86f1dcf1dcd206dc4e5 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -80,7 +80,7 @@ Section refcell_inv.
     iAssert (□ (&{α}((l +ₗ 1) ↦∗: ty_own ty1 tid) -∗
                 &{α}((l +ₗ 1) ↦∗: ty_own ty2 tid)))%I as "#Hb".
     { iIntros "!# H". iApply bor_iff; last done.
-      iNext; iAlways; iSplit; iIntros "H"; iDestruct "H" as (vl) "[Hf H]"; iExists vl;
+      iNext; iModIntro; iSplit; iIntros "H"; iDestruct "H" as (vl) "[Hf H]"; iExists vl;
       iFrame; by iApply "Hown". }
     iDestruct "H" as (st) "H"; iExists st;
       iDestruct "H" as "($&$&H)"; destruct st as [[[[ν rw] q' ] n]|]; try done;
@@ -191,7 +191,7 @@ Section refcell.
     - iPureIntro. simpl. congruence.
     - destruct vl as [|[[]|]]=>//=. by iApply "Hown".
     - simpl. iDestruct "H" as (a γ) "[Ha H]". iExists a, γ. iFrame.
-      iApply na_bor_iff; last done. iNext; iAlways; iSplit; iIntros "H".
+      iApply na_bor_iff; last done. iNext; iModIntro; iSplit; iIntros "H".
       by iApply "Hty1ty2". by iApply "Hty2ty1".
   Qed.
   Lemma refcell_mono' E L ty1 ty2 :
diff --git a/theories/typing/lib/refcell/refmut.v b/theories/typing/lib/refcell/refmut.v
index 0f51cf44dc1a1b902ef5179bec3877ccb3993e76..3776c5e75e93959c19b05257c84a2b2a3fa5d461 100644
--- a/theories/typing/lib/refcell/refmut.v
+++ b/theories/typing/lib/refcell/refmut.v
@@ -87,14 +87,14 @@ Section refmut.
     intros α1 α2 Hα ty1 ty2. rewrite eqtype_unfold=>Hty. iIntros (q) "HL".
     iDestruct (Hty with "HL") as "#Hty". iDestruct (Hα with "HL") as "#Hα".
     iIntros "!# #HE". iDestruct ("Hα" with "HE") as "Hα1α2".
-    iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [|iSplit; iAlways].
+    iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [|iSplit; iModIntro].
     - done.
     - iIntros (tid [|[[]|][|[[]|][]]]) "H"=>//=.
       iDestruct "H" as (ν γ q' β ty') "(Hb & #H⊑ & #Hinv & Hν & Hown)".
       iExists ν, γ, q', β, ty'. iFrame "∗#". iSplit.
       + iApply bor_shorten; last iApply bor_iff; last done.
         * iApply lft_intersect_mono; first done. iApply lft_incl_refl.
-        * iNext; iAlways; iSplit; iIntros "H"; iDestruct "H" as (vl) "[??]";
+        * iNext; iModIntro; iSplit; iIntros "H"; iDestruct "H" as (vl) "[??]";
           iExists vl; iFrame; by iApply "Ho".
       + by iApply lft_incl_trans.
     - iIntros (κ tid l) "H /=". iDestruct "H" as (lv lrc) "H". iExists lv, lrc.
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 7b7b7785d0e1fa67b0a95a1490caef82605077b4..d54884597af255b162a4444211b07067939b48ea 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -285,8 +285,8 @@ Section refmut_functions.
     iDestruct ("Hclose3" with "Hαν") as "[Hα Hν]".
     iMod ("Hclose2" with "Hϝ HL") as "HL".
     wp_rec. iDestruct "Hr" as "[Hr Hr†]".
-    iDestruct "Hr" as (?) "[Hr H]". iDestruct "H" as (vl1 ? ->) "[Hr1' H]".
-    iDestruct "H" as (vl2 ? ->) "[Hr2' ->]".
+    iDestruct "Hr" as (?) "[Hr H]". iDestruct "H" as (vl1 vl1' ->) "[Hr1' H]".
+    iDestruct "H" as (vl2 vl2' ->) "[Hr2' ->]".
     destruct vl1 as [|[[|lr1|]|] []], vl2 as [|[[|lr2|]|] []]=>//=.
     rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
     iDestruct "Hr" as "[Hr1 Hr2]". wp_read. wp_let. wp_op. wp_read. wp_let.
@@ -302,14 +302,14 @@ Section refmut_functions.
     destruct st as [[[[??]?]?]|]; last by destruct Hst as [[?|] Hst]; inversion Hst.
     move:Hst=>/Some_pair_included [/Some_pair_included_total_1
               [/to_agree_included /(leibniz_equiv _ _) [= <- <-] _] _].
-    iDestruct "Hst" as "(H† & Hq & _)". iDestruct "Hq" as (q' Hqq') "[Hν1 Hν2]".
+    iDestruct "Hst" as "(H† & Hq & _)". iDestruct "Hq" as (q1 Hqq1) "[Hν1 Hν2]".
     iMod (own_update with "H●") as "[H● ?]".
     { apply auth_update_alloc,
-         (op_local_update_discrete _ _ (writing_stR (q'/2)%Qp ν))=>-[Hagv _].
+         (op_local_update_discrete _ _ (writing_stR (q1/2)%Qp ν))=>-[Hagv _].
       split; [split|done].
       - by rewrite /= agree_idemp.
-      - apply frac_valid'. rewrite -Hqq' comm -{2}(Qp_div_2 q').
-        apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q'/2)%Qp).
+      - apply frac_valid'. rewrite -Hqq1 comm -{2}(Qp_div_2 q1).
+        apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q1/2)%Qp).
         apply Qcplus_le_mono_r, Qp_ge_0. }
     wp_let. wp_read. wp_let. wp_op. wp_write.
     wp_apply (wp_delete _ _ _ _ [_; _] with "[Hrefmut↦1 Hrefmut↦2 Hrefmut†]")=>//.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index d7b5b5fdbc10fac39eeb7dd909dfe8a321c9083d..0469dc74c242bc77d5e51c9662b30e6ba83cef34 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -82,7 +82,7 @@ Section rwlockreadguard.
     iDestruct (proj1 Hty with "HL") as "#Hty". iDestruct (Hα with "HL") as "#Hα".
     iDestruct (rwlock_proto_proper with "HL") as "#Hty1ty2"; first done.
     iIntros "!# #HE". iDestruct ("Hα" with "HE") as "Hα1α2".
-    iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [|iSplit; iAlways].
+    iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [|iSplit; iModIntro].
     - done.
     - iIntros (tid [|[[]|][]]) "H"; try done.
       iDestruct "H" as (ν q' γs β) "(#Hshr & #H⊑ & Htok & Hown & Hinh & Hinv)".
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index baa572274b98d8aa8392daf2e0abb9b1c8f1dc45..6cfd2e84803412f84fcbb7cb3eb66960afd5b035 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -82,12 +82,12 @@ Section rwlockwriteguard.
     iDestruct (Hty' with "HL") as "#Hty". iDestruct (Hα with "HL") as "#Hα".
     iDestruct (rwlock_proto_proper with "HL") as "#Hty1ty2"; first done.
     iIntros "!# #HE". iDestruct ("Hα" with "HE") as "Hα1α2".
-    iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [done|iSplit; iAlways].
+    iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [done|iSplit; iModIntro].
     - iIntros (tid [|[[]|][]]) "H"; try done.
       iDestruct "H" as (γs β) "(Hb & #H⊑ & Hown & Hinv)".
       iExists γs, β. iFrame "Hown". iSplitL "Hb"; last iSplitR "Hinv".
       + iApply bor_iff; last done.
-        iNext; iAlways; iSplit; iIntros "H"; iDestruct "H" as (vl) "[??]";
+        iNext; iModIntro; iSplit; iIntros "H"; iDestruct "H" as (vl) "[??]";
         iExists vl; iFrame; by iApply "Ho".
       + by iApply lft_incl_trans.
       + iDestruct "Hinv" as (γ tyO tyS) "(W & inv)".
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index 772d602e255c05626f1f65088d87c64084873257..2da54c522e52cc2241f187d00da96e1419e850c4 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -30,7 +30,7 @@ Section join_handle.
   Lemma join_handle_subtype ty1 ty2 :
     ▷ type_incl ty1 ty2 -∗ type_incl (join_handle ty1) (join_handle ty2).
   Proof.
-    iIntros "#Hincl". iSplit; first done. iSplit; iAlways.
+    iIntros "#Hincl". iSplit; first done. iSplit; iModIntro.
     - iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
       simpl. iDestruct "Hvl" as (γc γe) "Hvl". iExists γc, γe.
       iApply (join_handle_impl with "[] Hvl"). iIntros "!# * Hown" (tid').
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 0677b4332d1ae712636700caea1f2e63a4dd3b35..03080ae65c8b0d0de2dfc28eb85eb8651f3170f1 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -94,7 +94,7 @@ Section own.
   Lemma own_type_incl n m ty1 ty2 :
     ▷ ⌜n = m⌝ -∗ ▷ type_incl ty1 ty2 -∗ type_incl (own_ptr n ty1) (own_ptr m ty2).
   Proof.
-    iIntros "#Heq (#Hsz & #Ho & #Hs)". iSplit; first done. iSplit; iAlways.
+    iIntros "#Heq (#Hsz & #Ho & #Hs)". iSplit; first done. iSplit; iModIntro.
     - iIntros (?[|[[| |]|][]]) "H"; try done. simpl.
       iDestruct "H" as "[Hmt H†]". iNext. iDestruct ("Hsz") as %<-.
       iDestruct "Heq" as %->. iFrame. iApply (heap_mapsto_pred_wand with "Hmt").
@@ -141,7 +141,7 @@ Section own.
     Sync ty → Sync (own_ptr n ty).
   Proof.
     iIntros (Hsync κ tid1 tid2 l) "H". iDestruct "H" as (l') "[Hm #Hshr]".
-    iExists _. iFrame "Hm". iAlways. iIntros (F q) "% Htok".
+    iExists _. iFrame "Hm". iModIntro. iIntros (F q) "% Htok".
     iMod ("Hshr" with "[] Htok") as "Hfin"; first done. iModIntro. iNext.
     iMod "Hfin" as "{Hshr} [Hshr $]". by iApply Hsync.
   Qed.
@@ -241,7 +241,7 @@ Section typing.
   Lemma read_own_move E L ty n :
     ⊢ typed_read E L (own_ptr n ty) ty (own_ptr n $ uninit ty.(ty_size)).
   Proof.
-    rewrite typed_read_eq. iAlways.
+    rewrite typed_read_eq. iModIntro.
     iIntros ([[]|] tid F qL ?) "_ _ $ $ Hown"; try done.
     iDestruct "Hown" as "[H↦ H†]". iDestruct "H↦" as (vl) "[>H↦ Hown]".
     iDestruct (ty_size_eq with "Hown") as "#>%".
diff --git a/theories/typing/product.v b/theories/typing/product.v
index 9abc418ecd44b5ac99850728454d2bfa88ecdc3d..3bc52cac881b9db479202bde8509e2b45e4d3f02 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -94,7 +94,7 @@ Section product.
     iClear "∗". iIntros "!# #HE".
     iDestruct ("H1" with "HE") as "#(% & #Ho1 & #Hs1)". clear H1.
     iDestruct ("H2" with "HE") as "#(% & #Ho2 & #Hs2)". clear H2.
-    iSplit; first by (iPureIntro; simpl; f_equal). iSplit; iAlways.
+    iSplit; first by (iPureIntro; simpl; f_equal). iSplit; iModIntro.
     - iIntros (??) "H". iDestruct "H" as (vl1 vl2) "(% & Hown1 & Hown2)".
       iExists _, _. iSplit. done. iSplitL "Hown1".
       + by iApply "Ho1".
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index bbfa4ab43b14e03f07a2094d64b18947bdabcdde..8af91c2efb6c4c1c67815daf5c4b243ae8981f8c 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -130,7 +130,7 @@ Section sum.
     { iInduction Htyl as [|???? Hsub] "IH".
       { iClear "∗". iIntros "!# _". done. }
       iDestruct (Hsub with "HL") as "#Hsub". iDestruct ("IH" with "HL") as "{IH} #IH".
-      iAlways. iIntros "#HE". iDestruct ("Hsub" with "HE") as "(% & _ & _)".
+      iModIntro. iIntros "#HE". iDestruct ("Hsub" with "HE") as "(% & _ & _)".
       iDestruct ("IH" with "HE") as %IH. iPureIntro. simpl. inversion_clear IH. by f_equal. }
     iDestruct (subtype_Forall2_llctx with "HL") as "#Htyl"; first done.
     iClear "HL". iIntros "!# #HE".
@@ -146,11 +146,11 @@ Section sum.
         rewrite (nth_lookup_Some tyl2 _ _ ty2) //. }
     clear -Hleq. iClear "∗". iSplit; last iSplit.
     - simpl. by rewrite Hleq.
-    - iAlways. iIntros (tid vl) "H". iDestruct "H" as (i vl' vl'') "(% & % & Hown)".
+    - iModIntro. iIntros (tid vl) "H". iDestruct "H" as (i vl' vl'') "(% & % & Hown)".
       iExists i, vl', vl''. iSplit; first done.
       iSplit; first by rewrite -Hleq.
       iDestruct ("Hty" $! i) as "(_ & #Htyi & _)". by iApply "Htyi".
-    - iAlways. iIntros (κ tid l) "H". iDestruct "H" as (i) "(Hmt & Hshr)".
+    - iModIntro. iIntros (κ tid l) "H". iDestruct "H" as (i) "(Hmt & Hshr)".
       iExists i. iSplitR "Hshr".
       + rewrite /is_pad -Hleq. iDestruct ("Hty" $! i) as "(Hlen & _)".
         iDestruct "Hlen" as %<-. done.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 7515f0b35361b6d3c0c381f9b0e516ad3c8d41d0..b4fe9a2dd59cf602ba110d0465c2cfc9218e7fdc 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -551,14 +551,14 @@ Section subtyping.
   Global Instance type_incl_persistent ty1 ty2 : Persistent (type_incl ty1 ty2) := _.
 
   Lemma type_incl_refl ty : ⊢ type_incl ty ty.
-  Proof. iSplit; first done. iSplit; iAlways; iIntros; done. Qed.
+  Proof. iSplit; first done. iSplit; iModIntro; iIntros; done. Qed.
 
   Lemma type_incl_trans ty1 ty2 ty3 :
     type_incl ty1 ty2 -∗ type_incl ty2 ty3 -∗ type_incl ty1 ty3.
   Proof.
     iIntros "(% & #Ho12 & #Hs12) (% & #Ho23 & #Hs23)".
     iSplit; first (iPureIntro; etrans; done).
-    iSplit; iAlways; iIntros.
+    iSplit; iModIntro; iIntros.
     - iApply "Ho23". iApply "Ho12". done.
     - iApply "Hs23". iApply "Hs12". done.
   Qed.
@@ -646,7 +646,7 @@ Section subtyping.
     □ (∀ tid vl, st1.(st_own) tid vl -∗ st2.(st_own) tid vl) -∗
     type_incl st1 st2.
   Proof.
-    iIntros "#Hst". iSplit; first done. iSplit; iAlways.
+    iIntros "#Hst". iSplit; first done. iSplit; iModIntro.
     - iIntros. iApply "Hst"; done.
     - iIntros (???). iDestruct 1 as (vl) "[Hf Hown]". iExists vl. iFrame "Hf".
       by iApply "Hst".
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index e0cde6e6f88980260c2e0e595a4dda1963222792..2667230f1b6c2f1f0b00a42f10e3002520c73465 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -50,10 +50,10 @@ Section uniq_bor.
     iDestruct (Hty with "HL") as "#Hty". iDestruct (Hκ with "HL") as "#Hκ".
     iIntros "!# #HE". iSplit; first done.
     iDestruct ("Hty" with "HE") as "(_ & #Ho & #Hs)"; [done..|clear Hty].
-    iSpecialize ("Hκ" with "HE"). iSplit; iAlways.
+    iSpecialize ("Hκ" with "HE"). iSplit; iModIntro.
     - iIntros (? [|[[]|][]]) "H"; try done.
       iApply (bor_shorten with "Hκ"). iApply bor_iff; last done.
-      iNext. iAlways. iSplit; iIntros "H"; iDestruct "H" as (vl) "[??]";
+      iNext. iModIntro. iSplit; iIntros "H"; iDestruct "H" as (vl) "[??]";
       iExists vl; iFrame; by iApply "Ho".
     - iIntros (κ ??) "H". iAssert (κ2 ⊓ κ ⊑ κ1 ⊓ κ)%I as "#Hincl'".
       { iApply lft_intersect_mono. done. iApply lft_incl_refl. }
@@ -80,7 +80,7 @@ Section uniq_bor.
     Send ty → Send (uniq_bor κ ty).
   Proof.
     iIntros (Hsend tid1 tid2 [|[[]|][]]) "H"; try done.
-    iApply bor_iff; last done. iNext. iAlways. iApply bi.equiv_iff.
+    iApply bor_iff; last done. iNext. iModIntro. iApply bi.equiv_iff.
     do 3 f_equiv. iSplit; iIntros "."; by iApply Hsend.
   Qed.
 
@@ -88,7 +88,7 @@ Section uniq_bor.
     Sync ty → Sync (uniq_bor κ ty).
   Proof.
     iIntros (Hsync κ' tid1 tid2 l) "H". iDestruct "H" as (l') "[Hm #Hshr]".
-    iExists l'. iFrame "Hm". iAlways. iIntros (F q) "% Htok".
+    iExists l'. iFrame "Hm". iModIntro. iIntros (F q) "% Htok".
     iMod ("Hshr" with "[] Htok") as "Hfin"; first done. iClear "Hshr".
     iModIntro. iNext. iMod "Hfin" as "[Hshr $]". iApply Hsync. done.
   Qed.