diff --git a/opam b/opam
index 2a4f855ecbef2895e59e2a14ea7144c286939cc3..2c4ff15500a33cd8d3d7532b3ef8dee22e568f26 100644
--- a/opam
+++ b/opam
@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/actris" ]
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2020-11-26.2.03b317f4") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2020-12-04.7.68955c65") | (= "dev") }
 ]
diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index 646de1070ecd6c22f2d1b512aa0c9625cfdf2bd1..069d9fea9982e06f947570e4ef76ed3b3d5985bd 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -284,27 +284,27 @@ Section channel.
     - wp_apply (lisnil_spec with "Hr"); iIntros "Hr".
       destruct vsr as [|vr vsr]; wp_pures.
       { wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
-        iIntros "_". wp_pures. iApply "HΦ". iLeft. iSplit; [done|].
+        iIntros "_". wp_pures. iModIntro. iApply "HΦ". iLeft. iSplit; [done|].
         iExists γ, Left, l, r, lk. eauto 10 with iFrame. }
       wp_apply (lpop_spec with "Hr"); iIntros (v') "[% Hr]"; simplify_eq/=.
       iMod (iProto_recv_l with "Hctx H") as (q) "(Hctx & H & Hm)". wp_pures.
       rewrite iMsg_base_eq.
       iDestruct (iMsg_texist_exist with "Hm") as (x <-) "[Hp HP]".
       wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
-      iIntros "_". wp_pures. iApply "HΦ". iRight. iExists x. iSplit; [done|].
+      iIntros "_". wp_pures. iModIntro. iApply "HΦ". iRight. iExists x. iSplit; [done|].
       iFrame "HP". iExists γ, Left, l, r, lk. iSplit; [done|]. iFrame "Hlk".
       by iRewrite "Hp".
     - wp_apply (lisnil_spec with "Hl"); iIntros "Hl".
       destruct vsl as [|vl vsl]; wp_pures.
       { wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
-        iIntros "_". wp_pures. iApply "HΦ". iLeft. iSplit; [done|].
+        iIntros "_". wp_pures. iModIntro. iApply "HΦ". iLeft. iSplit; [done|].
         iExists γ, Right, l, r, lk. eauto 10 with iFrame. }
       wp_apply (lpop_spec with "Hl"); iIntros (v') "[% Hl]"; simplify_eq/=.
       iMod (iProto_recv_r with "Hctx H") as (q) "(Hctx & H & Hm)". wp_pures.
       rewrite iMsg_base_eq.
       iDestruct (iMsg_texist_exist with "Hm") as (x <-) "[Hp HP]".
       wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
-      iIntros "_". wp_pures. iApply "HΦ". iRight. iExists x. iSplit; [done|].
+      iIntros "_". wp_pures. iModIntro. iApply "HΦ". iRight. iExists x. iSplit; [done|].
       iFrame "HP". iExists γ, Right, l, r, lk. iSplit; [done|]. iFrame "Hlk".
       by iRewrite "Hp".
   Qed.
@@ -317,7 +317,7 @@ Section channel.
     iIntros (Φ) "Hc HΦ". iLöb as "IH". wp_lam.
     wp_apply (try_recv_spec with "Hc"); iIntros (w) "[[-> H]|H]".
     { wp_pures. by iApply ("IH" with "[$]"). }
-    iDestruct "H" as (x ->) "[Hc HP]". wp_pures. iApply "HΦ". iFrame.
+    iDestruct "H" as (x ->) "[Hc HP]". wp_pures. iApply "HΦ". by iFrame.
   Qed.
 
   (** ** Specifications for choice *)
diff --git a/theories/examples/sort.v b/theories/examples/sort.v
index 7e6da32f8bce5fec9532f087099424b42d3ce428..d64765da8929d9d7937f7c69ba52b0f2049756c0 100644
--- a/theories/examples/sort.v
+++ b/theories/examples/sort.v
@@ -70,7 +70,7 @@ Section sort.
       iApply "HΨ". iFrame. by rewrite list_merge_nil_l. }
     wp_apply (lisnil_spec with "Hl2"); iIntros "Hl2".
     destruct xs2 as [|x2 xs2]; wp_pures.
-    { iApply "HΨ". iFrame. }
+    { iApply "HΨ". by iFrame. }
     wp_apply (lhead_spec_aux with "Hl1"); iIntros (v1 l1') "[HIx1 Hl1]".
     wp_apply (lhead_spec_aux with "Hl2"); iIntros (v2 l2') "[HIx2 Hl2]".
     wp_apply ("Hcmp" with "[$HIx1 $HIx2]"); iIntros "[HIx1 HIx2] /=".
@@ -147,6 +147,6 @@ Section sort.
     wp_send with "[$Hcmp]".
     wp_send with "[$Hl]".
     wp_recv (ys) as "(Hsorted & Hperm & Hl)".
-    iApply "HΦ"; iFrame.
+    iApply "HΦ"; by iFrame.
   Qed.
 End sort.
diff --git a/theories/examples/sort_fg.v b/theories/examples/sort_fg.v
index af8d0df672fa2e528f5bdd002fb14be9fcb608e5..c8d0670b7f876acadaa2dc08f68cba7278671b72 100644
--- a/theories/examples/sort_fg.v
+++ b/theories/examples/sort_fg.v
@@ -159,7 +159,7 @@ Section sort_fg.
         inversion 1; discriminate_list || simplify_list_eq. by constructor.
     - wp_select with "[]".
       { by rewrite /= Hys Hxs Hys'. }
-      iApply "HΨ". iFrame.
+      iApply "HΨ". by iFrame.
   Qed.
 
   Lemma sort_service_fg_merge_spec cmp c p c1 c2 xs ys xs1 xs2 y1 w1 ys1 ys2 :
@@ -249,7 +249,7 @@ Section sort_fg.
     iIntros (Φ) "[Hl Hc] HΦ".
     iInduction xs as [|x xs] "IH" forall (xs').
     { wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl"; wp_pures.
-      iApply "HΦ". rewrite right_id_L. iFrame. }
+      iApply "HΦ". rewrite right_id_L. by iFrame. }
     wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl". wp_select.
     wp_apply (lpop_spec with "Hl"); iIntros (v) "[HIx Hl]".
     wp_send with "[$HIx]". wp_apply ("IH" with "Hl Hc"). by rewrite -assoc_L.
diff --git a/theories/examples/swap_mapper.v b/theories/examples/swap_mapper.v
index cfeecaa2e73b4ebe629e6d5ba1622f9a702af168..0b21edf08005ced29ad2e2e569f80847fcfdf3ed 100644
--- a/theories/examples/swap_mapper.v
+++ b/theories/examples/swap_mapper.v
@@ -221,7 +221,7 @@ Section with_Σ.
     iIntros (Φ) "[Hl Hc] HΦ".
     iInduction xs as [|x xs] "IH" forall (xs').
     { wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl"; wp_pures.
-      iApply "HΦ". iFrame. }
+      iApply "HΦ". by iFrame. }
     wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl".
     wp_send with "[//]".
     wp_apply (lpop_spec with "Hl"); iIntros (v) "[HIx Hl]".
diff --git a/theories/logrel/examples/compute_client_list.v b/theories/logrel/examples/compute_client_list.v
index e24e07d1cbc8b65c5882c2bdda544b4951317ea6..4f37e567f7205fd7374d3302fdebf28e2d7f6b56 100644
--- a/theories/logrel/examples/compute_client_list.v
+++ b/theories/logrel/examples/compute_client_list.v
@@ -187,7 +187,7 @@ Section compute_example.
         iExists n, false.
         rewrite lookup_total_insert -lsty_car_app lty_app_end_l lty_app_end_r.
         iFrame "Hf Hcounter Hc". }
-      iIntros "_". wp_pures. iApply "HΦ". iFrame "Hl Hlk Hsf". }
+      iIntros "_". wp_pures. iApply "HΦ". by iFrame "Hl Hlk". }
     wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl".
     wp_apply (acquire_spec with "Hlk").
     iIntros "[Hlocked HI]".
diff --git a/theories/logrel/examples/mapper_list.v b/theories/logrel/examples/mapper_list.v
index 2d114dfe788c16ba74c3eff9f08064a87317fb8c..1703f718bfccd638929f704f4aa488051dba567c 100644
--- a/theories/logrel/examples/mapper_list.v
+++ b/theories/logrel/examples/mapper_list.v
@@ -245,7 +245,7 @@ Section mapper_example.
     iIntros (Φ) "[Hl Hc] HΦ".
     iInduction xs as [|x xs] "IH".
     { wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl"; wp_pures.
-      iApply "HΦ". iFrame. }
+      iApply "HΦ". by iFrame. }
     wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl".
     rewrite /select.
     wp_send with "[]"; first by eauto.
@@ -268,7 +268,7 @@ Section mapper_example.
     iIntros (Φ) "[Hl Hc] HΦ".
     iInduction xs as [|x xs] "IH" forall (n).
     { wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl"; wp_pures.
-      iApply "HΦ". iFrame. }
+      iApply "HΦ". by iFrame. }
     wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl".
     simpl.
     iDestruct (iProto_mapsto_le c with "Hc []") as "Hc".
diff --git a/theories/logrel/examples/par_recv.v b/theories/logrel/examples/par_recv.v
index daba98ef3f9e98912c7e3ea7b8b2b441025462f8..6c932d4d84a51f20519f8120d97c5d367e47566e 100755
--- a/theories/logrel/examples/par_recv.v
+++ b/theories/logrel/examples/par_recv.v
@@ -163,7 +163,7 @@ Section double_fc.
           as "[Hγ1a Hγ1b]"; [by apply cmra_update_exclusive|].
         wp_apply (release_spec with "[$Hlock $Hlocked Hγ1a Hc]").
         { iRight. iLeft. iExists true, v. iFrame. }
-        iIntros "_". wp_pures. iLeft. iFrame.
+        iIntros "_". wp_pures. iLeft. by iFrame.
       + iDestruct "Hc" as ([] v) "[Hγ2 Hc]".
         { by iDestruct (own_valid_2 with "Hγ1 Hγ2") as %[]. }
         wp_recv (v') as "HP". wp_pures.
@@ -173,7 +173,7 @@ Section double_fc.
         iDestruct "Hγ2" as "[Hγ2a Hγ2b]".
         wp_apply (release_spec with "[$Hlock $Hlocked Hγ1a Hγ2a Hc]").
         { do 2 iRight. iExists v', v. iFrame. }
-        iIntros "_". wp_pures. iRight. iExists v. iFrame.
+        iIntros "_". wp_pures. iRight. iExists v. by iFrame.
       + iDestruct "Hc" as (v v') "[Hγ1' _]".
         by iDestruct (own_valid_2 with "Hγ1 Hγ1'") as %[].
     - (* Acquire lock *)
@@ -185,7 +185,7 @@ Section double_fc.
           as "[Hγ2a Hγ2b]"; [by apply cmra_update_exclusive|].
         wp_apply (release_spec with "[$Hlock $Hlocked Hγ2a Hc]").
         { iRight. iLeft. iExists false, v. iFrame. }
-        iIntros "_". wp_pures. iLeft. iFrame.
+        iIntros "_". wp_pures. iLeft. by iFrame.
       + iDestruct "Hc" as ([] v) "[Hγ1 Hc]"; last first.
         { by iDestruct (own_valid_2 with "Hγ1 Hγ2") as %[]. }
         wp_recv (v') as "HP". wp_pures.
@@ -195,7 +195,7 @@ Section double_fc.
         iDestruct "Hγ1" as "[Hγ1a Hγ1b]".
         wp_apply (release_spec with "[$Hlock $Hlocked Hγ1a Hγ2a Hc]").
         { do 2 iRight. iExists v, v'. iFrame. }
-        iIntros "_". wp_pures. iRight. iExists v. iFrame.
+        iIntros "_". wp_pures. iRight. iExists v. by iFrame.
       + iDestruct "Hc" as (v v') "(_ & Hγ2' & _)".
         by iDestruct (own_valid_2 with "Hγ2 Hγ2'") as %[].
     - iIntros (v1 v2) "[[[H1 Hγ]|H1] [[H2 Hγ']|H2]] !>".
diff --git a/theories/logrel/lib/mutex.v b/theories/logrel/lib/mutex.v
index 839c7b0e7b14782bc3d620b563d648f5aabc3511..02d2ee1b19f6388885aa165c78ecf1cad3296e84 100644
--- a/theories/logrel/lib/mutex.v
+++ b/theories/logrel/lib/mutex.v
@@ -125,7 +125,7 @@ Section rules.
     wp_apply (acquire_spec with "Hlock"); iIntros "[Hlocked Hinner]".
     iDestruct "Hinner" as (v) "[Hl HA]".
     wp_load. iFrame "HA". iApply ctx_ltyped_cons.
-    iFrame "HΓ". iExists _; iSplit; [done|]. iExists γ, l, lk, v. auto with iFrame.
+    iFrame "HΓ". iModIntro. iExists _; iSplit; [done|]. iExists γ, l, lk, v. auto with iFrame.
   Qed.
 
   Lemma ltyped_mutex_release Γ Γ' (x : string) e A :
diff --git a/theories/logrel/session_typing_rules.v b/theories/logrel/session_typing_rules.v
index 6b7be5e46cfc05f73831b4917878b153632a63d2..9d98145634bdcb7ba14dd191d4565f6cedf6cf38 100644
--- a/theories/logrel/session_typing_rules.v
+++ b/theories/logrel/session_typing_rules.v
@@ -98,7 +98,7 @@ Section session_typing_rules.
     iIntros (HΓx%ctx_lookup_perm Hin); iIntros "!>" (vs) "HΓ /=".
     rewrite {1}HΓx /=.
     iDestruct (ctx_ltyped_cons with "HΓ") as (c Hvs) "[Hc HΓ]". rewrite Hvs.
-    rewrite /select. wp_send with "[]"; [by eauto|]. iSplit; [done|].
+    rewrite /select. wp_send with "[]"; [by eauto|]. iModIntro. iSplit; [done|].
     iDestruct (ctx_ltyped_insert _ _ x (chan _) with "[Hc //] HΓ") as "HΓ' /=".
     by rewrite insert_id // lookup_total_alt Hin.
   Qed.
@@ -116,7 +116,7 @@ Section session_typing_rules.
     WP subst_map ws (switch_lams y i (S (length As)) e)
       {{ ltty_car (lty_arr_list (A :: As) B) }}.
   Proof.
-    iIntros "H". wp_pures. iIntros (v) "HA".
+    iIntros "H". wp_pures. iIntros "!>" (v) "HA".
     iDestruct ("H" with "HA") as "H".
     rewrite subst_map_insert.
     wp_apply "H".
diff --git a/theories/logrel/term_typing_rules.v b/theories/logrel/term_typing_rules.v
index f67b1c4d6a3fde96e308a835b7bcdf06b5d6e4ac..da08a29eb1d3edc98e5456ce4e8f75191513331e 100644
--- a/theories/logrel/term_typing_rules.v
+++ b/theories/logrel/term_typing_rules.v
@@ -136,7 +136,7 @@ Section term_typing_rules.
   Proof.
     iIntros "#He" (vs) "!> HΓ /=". wp_pures.
     iDestruct (ctx_ltyped_app with "HΓ") as "[HΓ1 $]".
-    iIntros (v) "HA1". wp_pures.
+    iIntros "!>" (v) "HA1". wp_pures.
     iDestruct ("He" $! (binder_insert x v vs) with "[HA1 HΓ1]") as "He'".
     { by iApply (ctx_ltyped_insert' with "HA1"). }
     rewrite subst_map_binder_insert.
@@ -172,7 +172,7 @@ Section term_typing_rules.
       iApply (big_sepL_impl with "HΓ1"). iIntros "!>" (k [y B] _) "/=".
       iDestruct 1 as (v ?) "HB". iExists v. iSplit; [by auto|].
       by iDestruct (coreP_intro with "HB") as "{HB} #HB". }
-    iLöb as "IH".
+    iModIntro. iLöb as "IH".
     iIntros (v) "!> HA1". wp_pures. set (r := RecV f x _).
     iDestruct ("He" $! (binder_insert f r (binder_insert x v vs))
       with "[HΓ1 HA1]") as "He'".
@@ -245,7 +245,7 @@ Section term_typing_rules.
     iDestruct (ctx_ltyped_cons with "HΓ") as (v Hvs) "[HA HΓ]"; rewrite Hvs.
     iDestruct "HA" as (v1 v2 ->) "[HA1 HA2]". wp_pures.
     iAssert (ltty_car (copy- A1) v1)%lty as "#HA1m"; [by iApply coreP_intro|].
-    iFrame "HA1". iApply ctx_ltyped_cons. iExists _; iSplit; [done|]; iFrame "HΓ".
+    iFrame "HA1". iApply ctx_ltyped_cons. iModIntro. iExists _; iSplit; [done|]; iFrame "HΓ".
     iExists v1, v2. eauto with iFrame.
   Qed.
 
@@ -257,7 +257,7 @@ Section term_typing_rules.
     iDestruct (ctx_ltyped_cons with "HΓ") as (v Hvs) "[HA HΓ]"; rewrite Hvs.
     iDestruct "HA" as (v1 v2 ->) "[HA1 HA2]". wp_pures.
     iAssert (ltty_car (copy- A2) v2)%lty as "#HA2m"; [by iApply coreP_intro|].
-    iFrame "HA2". iApply ctx_ltyped_cons. iExists _; iSplit; [done|]; iFrame "HΓ".
+    iFrame "HA2". iApply ctx_ltyped_cons. iModIntro. iExists _; iSplit; [done|]; iFrame "HΓ".
     iExists v1, v2. eauto with iFrame.
   Qed.
 
@@ -304,7 +304,7 @@ Section term_typing_rules.
   Proof.
     iIntros "#He" (vs) "!> HΓ /=". wp_pures.
     iDestruct (ctx_ltyped_app with "HΓ") as "[HΓ1 $]".
-    iIntros (M) "/=". wp_pures.
+    iIntros "!>" (M) "/=". wp_pures.
     iApply (wp_wand with "(He HΓ1)"). iIntros (v) "[$ _]".
   Qed.
 
@@ -369,7 +369,7 @@ Section term_typing_rules.
     iDestruct (ctx_ltyped_cons with "HΓ") as (v Hvs) "[HA HΓ]"; rewrite Hvs.
     iDestruct "HA" as (l w ->) "[? HA]". wp_load.
     iAssert (ltty_car (copy- A) w)%lty as "#HAm"; [by iApply coreP_intro|].
-    iFrame "HA". iApply ctx_ltyped_cons. iExists _; iSplit; [done|]; iFrame "HΓ".
+    iFrame "HA". iApply ctx_ltyped_cons. iModIntro. iExists _; iSplit; [done|]; iFrame "HΓ".
     iExists l, w. eauto with iFrame.
   Qed.
 
@@ -382,7 +382,7 @@ Section term_typing_rules.
     wp_apply (wp_wand with "(He HΓ)"). iIntros (v) "[HB HΓ']".
     rewrite {2}HΓx /=.
     iDestruct (ctx_ltyped_cons with "HΓ'") as (vl Hvs) "[HA HΓ']"; rewrite Hvs.
-    iDestruct "HA" as (l w ->) "[? HA]". wp_store. iSplit; [done|].
+    iDestruct "HA" as (l w ->) "[? HA]". wp_store. iModIntro. iSplit; [done|].
     iApply ctx_ltyped_cons. iExists _; iSplit; [done|]; iFrame "HΓ'".
     iExists l, v. eauto with iFrame.
   Qed.
diff --git a/theories/utils/llist.v b/theories/utils/llist.v
index 7c1122d0a064c2bb055fecc878fa6bbb3716b8c3..0428f6b0f85a2127af989ea3fe4e76bf589edce4 100644
--- a/theories/utils/llist.v
+++ b/theories/utils/llist.v
@@ -237,8 +237,8 @@ Proof.
   iIntros (Φ) "Hll HΦ".
   iInduction xs as [|x xs] "IH" forall (l n Φ); simpl; wp_rec; wp_pures.
   - destruct n as [|n]; simpl; wp_pures.
-    + wp_load. wp_alloc k. wp_store. iApply "HΦ"; iFrame.
-    + wp_load. wp_alloc k. iApply "HΦ"; iFrame.
+    + wp_load. wp_alloc k. wp_store. iApply "HΦ"; by iFrame.
+    + wp_load. wp_alloc k. iApply "HΦ"; by iFrame.
   - iDestruct "Hll" as (v l') "(HIx & Hl & Hll)". destruct n as [|n]; simpl; wp_pures.
     + wp_load. wp_alloc k. wp_store. iApply "HΦ"; eauto with iFrame.
     + wp_load; wp_pures. rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.