diff --git a/opam b/opam
index 8565a7bab90647159d2369b93cd17deb9f61999e..437cfece431be49c0c6103c32cba4b64dba1ac0f 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/igps" ]
 depends: [
-  "coq-iris" { (= "branch.gen_proofmode.2018-03-02.0") | (= "dev") }
+  "coq-iris" { (= "branch.gen_proofmode.2018-03-03.3") | (= "dev") }
 ]
diff --git a/theories/base/fork.v b/theories/base/fork.v
index 7a79382425061abafee1e7348417460f0335b6d8..397c7d7f61d78686b5aeb44a968b5255a36d1237 100644
--- a/theories/base/fork.v
+++ b/theories/base/fork.v
@@ -21,7 +21,7 @@ Proof.
   iDestruct "HV" as "[HV FV]".
 
   iApply wp_fork_pst => //; first by exact: H0.
-  - iNext. iFrame "HoP".
+  - iFrame "HoP". iNext.
     iIntros (Ï‚' V') "(% & % & % & % & OÏ‚')". inversion H7. subst.
 
     have: (∃ ρ : thread, VIEW !! ρ = None) => [|[ρ Hρ]].
diff --git a/theories/escrows.v b/theories/escrows.v
index e457d11c30527a7bc05a3a22d64afd792722ba8e..3b6de32f8c907e57e2d5541afada5c9be7815b84 100644
--- a/theories/escrows.v
+++ b/theories/escrows.v
@@ -81,7 +81,7 @@ Section proof.
     iAssert (inv escrowN (monPred_at P V ∨ monPred_at Q V))%I with "[Inv]" as "#Inv'".
     { destruct b; subst P Q; auto. by rewrite bi.or_comm. }
     iClear "Inv". iInv escrowN as "Inv" "HClose".
-    iAssert (▷ Q V ∗ ▷ (P V ∨ Q V))%I with "[P Inv ND]" as "[Q Inv]".
+    iAssert (▷ (Q V ∗ (P V ∨ Q V)))%I with "[P Inv ND]" as "[Q Inv]".
       { iNext.
         iDestruct "Inv" as "[Inv|$]".
         - iExFalso. iApply ("ND" $! V0 with "[%//] [$P $Inv]").
@@ -130,7 +130,7 @@ Section proof.
     rewrite /escrow /exchange /=. iIntros (V ?) "(Esc & oP)".
     iDestruct "Esc" as (V') "[% ?]".
     iInv escrowN as "Inv" "HClose".
-    iAssert (▷ Q V' ∗ ▷ ((∃ᵢ P)%I V' ∨ Q V'))%I with "[ND oP Inv]" as "[Q Inv]".
+    iAssert (▷ (Q V' ∗ ((∃ᵢ P)%I V' ∨ Q V')))%I with "[ND oP Inv]" as "[Q Inv]".
       { iNext. iDestruct "Inv" as "[Inv|$]".
         - iExFalso.
           iDestruct "oP" as (V1) "P1".
diff --git a/theories/examples/circ_buffer.v b/theories/examples/circ_buffer.v
index 024842a680e317b8fb72fc32740d016467e98521..6d2b96b1ad6a5862e3352e0c6c480875ec07ea15 100644
--- a/theories/examples/circ_buffer.v
+++ b/theories/examples/circ_buffer.v
@@ -81,7 +81,7 @@ Section CircBuffer.
 
     Lemma pTok_exclusive γ i: ⎡pTok γ i⎤ ∗ ⎡pTok γ i⎤ ⊢ False : vProp Σ.
     Proof.
-      iIntros "Tok". rewrite -bi_embed_sep -own_op pair_op.
+      iIntros "Tok". rewrite -embed_sep -own_op pair_op.
       iDestruct (own_valid with "Tok") as %[Valid _]. simpl in Valid.
       rewrite -> coPset_disj_valid_op, disjoint_singleton_l in Valid.
       exfalso. by apply Valid, elem_of_singleton.
@@ -89,7 +89,7 @@ Section CircBuffer.
 
     Lemma cTok_exclusive γ i: ⎡cTok γ i⎤ ∗ ⎡cTok γ i⎤ ⊢ False : vProp Σ.
     Proof.
-      iIntros "Tok". rewrite -bi_embed_sep -own_op pair_op.
+      iIntros "Tok". rewrite -embed_sep -own_op pair_op.
       iDestruct (own_valid with "Tok") as %[_ Valid]. simpl in Valid.
       rewrite -> coPset_disj_valid_op, disjoint_singleton_l in Valid.
       exfalso. by apply Valid, elem_of_singleton.
@@ -286,7 +286,7 @@ Section CircBuffer.
       wp_lam. wp_bind ([_]_at)%E. wp_op.
 
       iApply (GPS_SW_Read_ex with "[$kI $pW]"); [done|done|..].
-      { rewrite /monPred_absolutely /=. iIntros (????) "!> #$ //". }
+      { rewrite monPred_absolutely_unfold. iIntros (????) "!> #$ //". }
 
       iNext. iIntros (w) "(pW & #CEs)".
       iDestruct "CEs" as "(% & CEs)".
@@ -296,9 +296,9 @@ Section CircBuffer.
 
       iApply (GPS_SW_Read (consInt γ q) True%I (CP (γ,q))
                 with "[$kI $cR]"); [done|done|..].
-      { iNext. iSplitL.
-        - iIntros (?). iIntros "_". iLeft. by iIntros (?) "(? & _)".
-        - rewrite /monPred_absolutely /=. iIntros (?????) "[? #$] //". }
+      { iSplitL.
+        - iIntros (?). iIntros "_". iLeft. by iIntros "!>" (?) "(? & _)".
+        - rewrite monPred_absolutely_unfold. iIntros "!>" (?????) "[? #$] //". }
 
       iNext. iIntros (j r) "(% & #cR2 & #PEs)".
       iDestruct "PEs" as "(% & PEs)".
@@ -358,7 +358,7 @@ Section CircBuffer.
         { rewrite Nat.add_1_r; apply Nat.le_succ_diag_r. }
         { iSplitR "".
           - iNext. iIntros (v5). iIntros "(#Px & _ & $)".
-            iModIntro. iNext. iSplitL ""; first done.
+            iModIntro. iSplitL ""; first done. iNext.
             iSplitL ""; iIntros "!#"; [by rewrite Nat2Z.inj_add|].
             cbn. iIntros (k). iIntros (Hk).
             iApply ("Px"). iPureIntro. lia'.
@@ -388,10 +388,9 @@ Section CircBuffer.
 
       iApply (GPS_SW_Read (prodInt P γ q) True%I (PP P (γ,q))
                 with "[$kI $pR]"); [done|done|..].
-      { iNext. iSplitL.
-        - iIntros (?). iIntros (?). iLeft.
-          iIntros (?) "(? & _)". by auto.
-        - rewrite /monPred_absolutely /=. iIntros (?????) "[? #$] //". }
+      { iSplitL.
+        - iIntros (??). iLeft. iIntros "!>" (?) "(? & _)". by auto.
+        - rewrite monPred_absolutely_unfold. iIntros "!>" (?????) "[? #$] //". }
 
       iNext. iIntros (i w) "(% & pR & #CEs)".
       iDestruct "CEs" as "(% & CEs)".
@@ -400,7 +399,7 @@ Section CircBuffer.
 
       iApply (GPS_SW_Read_ex
                 with "[$kI $cW]"); [done|done|..].
-      { rewrite /monPred_absolutely /=. iIntros (????) "!> #$ //". }
+      { rewrite monPred_absolutely_unfold. iIntros "!>" (????) "!> #$ //". }
 
       iNext. iIntros (r) "(cW & #PEs)".
       iDestruct "PEs" as "(% & PEs)".
@@ -466,7 +465,7 @@ Section CircBuffer.
         { rewrite Nat.add_1_r; apply Nat.le_succ_diag_r. }
         { iSplitR "".
           - iNext. iIntros (v5). iIntros "(#Px & _ & $)".
-            iModIntro. iNext. iSplitL ""; first auto.
+            iModIntro. iSplitL ""; first auto. iNext.
             iSplitL ""; iIntros "!#"; [by rewrite Nat2Z.inj_add|auto].
             cbn. iIntros (k). iIntros (Hk).
             iApply ("Px"). iPureIntro. lia'.
diff --git a/theories/examples/hashtable.v b/theories/examples/hashtable.v
index 62023fe5dad5f33cfaf74dc04257b8c156ab9334..c3e4fa93f5bb59860082640c1e8ca70429e24cb3 100644
--- a/theories/examples/hashtable.v
+++ b/theories/examples/hashtable.v
@@ -1801,7 +1801,7 @@ Section proof.
     apply exist_timeless; intro.
     apply sep_timeless; first apply _.
     apply sep_timeless.
-    { apply sbi_embed_timeless, own_timeless, @Excl_discrete.
+    { apply embed_timeless, own_timeless, @Excl_discrete.
       repeat intro.
       apply option_ofe_discrete; auto.
       apply _. }
@@ -2107,7 +2107,7 @@ Section proof.
       wp_seq.
       iApply wp_fork; first done.
       iSplit; first done.
-      iNext; iSplitL "Hpost Hentries Hhist Hprots Ht Hresults".
+      iSplitL "Hpost Hentries Hhist Hprots Ht Hresults".
       + iApply "Hpost".
         iSplit; first by iPureIntro; omega.
         rewrite Z2Nat.inj_add; try omega.
@@ -2118,7 +2118,7 @@ Section proof.
         * unfold base_mask; rewrite !disjoint_union_l.
           split; first by split; apply namespaces.ndot_ne_disjoint.
           apply namespaces.ndot_preserve_disjoint_l, namespaces.ndot_ne_disjoint; done.
-        * iNext; iIntros (?) "?"; done. }
+        * iIntros "!> !>" (?) "?"; done. }
     { simpl.
       change (seq 0 (Z.to_nat 0)) with (@nil nat); simpl.
       iSplit; first by iPureIntro; omega.
diff --git a/theories/examples/message_passing.v b/theories/examples/message_passing.v
index 9dcc9ddd1a03d0fe4fd3eebbed5d9e0f56f855f8..e4d570bb91ee26ee205ef7ba1a4741824d68dcdf 100644
--- a/theories/examples/message_passing.v
+++ b/theories/examples/message_passing.v
@@ -77,7 +77,7 @@ Section proof.
 
     iApply (GPS_PP_Init_default (mpInt x γ) false with "[kI $kIp] [$Nay]");
     [done|done|done|..].
-    { iNext. by iSplitL "". }
+    { by iSplitL "". }
 
     iNext. iIntros "#yPRT".
     wp_seq.
@@ -96,7 +96,7 @@ Section proof.
       + iSplitL.
         * iNext. iIntros (?). iIntros "_".
           iLeft. iIntros (?) "[YP  _]". by simpl.
-        * rewrite /monPred_absolutely /=. iIntros (?????) "!> [_ #$] //".
+        * rewrite monPred_absolutely_unfold /=. iIntros (?????) "!> [_ #$] //".
       + iNext. iIntros (s v) "(_ & #yPRT5 & #YP)".
         destruct s.
         * iDestruct "YP" as "(% & XE)".
diff --git a/theories/examples/msqueue.v b/theories/examples/msqueue.v
index d349367e55433e52455c818e8e6294323b1a918b..4e0db8c90b2bdaf26d121434d820d16a1b77b577 100644
--- a/theories/examples/msqueue.v
+++ b/theories/examples/msqueue.v
@@ -183,7 +183,7 @@ Section MSQueue.
 
       iApply (GPS_PP_Init (p:=γ) (Link P γ) Null
               with "[$kI $kP $os]"); [done|done|..].
-      { iNext. rewrite !(unf_int (Link P)) /=. by iSplit. }
+      { rewrite !(unf_int (Link P)) /=. by iSplit. }
       iNext. iIntros "#Links".
       wp_seq. wp_bind (malloc _).
 
@@ -230,7 +230,7 @@ Section MSQueue.
         [done|done|..].
       { iSplitL "".
         - iNext. iIntros ([] ?). iLeft. by iIntros (x) "($ & _)".
-        - rewrite /monPred_absolutely /=. iIntros (?????) "!> [_ #$] //". }
+        - rewrite monPred_absolutely_unfold /=. iIntros (?????) "!> [_ #$] //". }
       iNext. iIntros ([] x) "(_ & _ & % & ox)".
       wp_seq. wp_bind ([_]_at)%E. wp_op. wp_op.
       rewrite (_ : ZplusPos 0 (Z.to_pos x) = Z.to_pos (x + 0)); last first.
@@ -241,9 +241,8 @@ Section MSQueue.
                        ∗ ∃ γ', [PP Z.to_pos (z + link) in Null @ γ' | Link P γ']))%I.
       iApply (GPS_PP_Read (p:=γ) (Link P γ) True%I Q' with "kI [$ox]");
         [done|done|..].
-      { iNext. iSplitL "".
-        - iIntros (s'). iIntros "_". iLeft.
-          iIntros (v). iIntros "(LinkInt & _)".
+      { iSplitL "".
+        - iIntros (s') "_". iLeft. iIntros "!>"( v) "(LinkInt & _)".
           rewrite (unf_int (Link P)).
           iModIntro. iIntros "%". destruct s' as [|l'].
           + by iDestruct "LinkInt" as "%".
@@ -251,7 +250,7 @@ Section MSQueue.
             iDestruct "LinkInt" as (γ') "(_ & Link)".
             iSplitL ""; first (iPureIntro; lia).
             iExists γ'. subst v. iFrame "Link".
-        - rewrite /monPred_absolutely /=. iIntros (????) "_ (_ & #$) //". }
+        - rewrite monPred_absolutely_unfold /=. iIntros (????) "!> _ (_ & #$) //". }
 
       iNext. iIntros (s n') "(% & _ & Q)".
       wp_seq. wp_op; case_bool_decide.
@@ -265,7 +264,7 @@ Section MSQueue.
           [done|done|done|..].
         { iSplitR "Q"; last by iFrame "Q oT".
           iNext. iIntros "(Q & _)".
-          iSplitR "Q"; first done. iModIntro. iNext. iSplitR "Q"; first done.
+          iSplitR "Q"; first done. iModIntro. iSplitR "Q"; first done.
           by iApply ("Q" with "[%]"). }
 
         iNext. iIntros "oT2".
@@ -296,7 +295,7 @@ Section MSQueue.
       iMod (own_alloc (Excl ())) as (γ') "Tok"; first done.
       iApply (GPS_PP_Init (p:=γ')  (Link P γ') Null
                with "[$kI $kP $ol]"); [done|done|..].
-      { iNext. rewrite !(unf_int (Link P)). by iSplit. }
+      { rewrite !(unf_int (Link P)). by iSplit. }
 
       iNext. iIntros "Link'". wp_seq.
       wp_bind ((rec: "f" <> := _) _)%E.
@@ -325,7 +324,8 @@ Section MSQueue.
                   with "kI [P Tok od Link]");
           [done|done|..].
         { iFrame "Tok Link". iSplitR "P od"; last iSplitR "P od"; last first.
-          - rewrite /monPred_absolutely /=. iIntros "{$P $od}" (????) "!> _ (_ & #$) //".
+          - rewrite monPred_absolutely_unfold /=.
+            iIntros "{$P $od}" (????) "!> _ (_ & #$) //".
           - iNext. iIntros (??) "(_ & _ & _ & ? & ? & _)". by iFrame.
           - iNext. iIntros (s'). iIntros "(_ & LinkInt & P')".
             rewrite (unf_int (Link P)).
@@ -337,8 +337,7 @@ Section MSQueue.
               iDestruct (escrow_alloc (Tok γ) (∃ v, ZplusPos data n ↦ v ∗ P v ∗ Tok γ')%I with "[P']") as "DEQ".
               { iNext. iExists x. by iFrame "P'". }
               iMod (fupd_mask_mono with "DEQ") as "#DEQ"; first namespaces.solve_ndisj.
-              iModIntro. iNext.
-              rewrite !(unf_int (Link P)).
+              iModIntro. rewrite !(unf_int (Link P)).
               iSplitL ""; (iSplitL ""; first done);
                 iExists γ'; iFrame "DEQ"; iFrame "Link'".
             + iDestruct "LinkInt" as "(% & _)". exfalso. lia. }
@@ -349,9 +348,9 @@ Section MSQueue.
           iApply (GPS_PP_Write (p:=()) (Tail P) () True%I (λ _, True)%I
                 with "[$kI oT]");
                 [done|done|done|..].
-          { iFrame "oT". iNext. iSplitL; last done.
-            iIntros "_". iModIntro. iSplitL; first done.
-            iNext. iSplitL; first done. iSplitL.
+          { iFrame "oT". iSplitL; last done.
+            iIntros "!> _". iModIntro. iSplitL; first done.
+            iSplitL; first done. iSplitL.
             - iPureIntro. lia.
             - by iExists γ'. }
           iNext. iIntros "oT2".
@@ -374,9 +373,9 @@ Section MSQueue.
               ∗ (∃ γ : gname, [PP Z.to_pos (x + 0) in Null @ γ | Link P γ ]))%I.
       iApply (GPS_PP_Read (p:=()) (Head P) True%I Q with "kI [$oH]");
         [done|done|..].
-      { iNext. iSplitL.
-        - iIntros ([]) "_". iLeft. by iIntros (x) "($ & _)".
-        - rewrite /monPred_absolutely /=. iIntros (????) "_ (_ & #$) //". }
+      { iSplitL.
+        - iIntros ([]) "_". iLeft. by iIntros "!>" (x) "($ & _)".
+        - rewrite monPred_absolutely_unfold /=. iIntros "!>" (????) "_ (_ & #$) //". }
 
       iNext. iIntros ([] s) "(_ & oH2 & % & os)".
       iDestruct "os" as (γ) "os".
@@ -393,9 +392,9 @@ Section MSQueue.
                       ∗ [PP Z.to_pos (n + link) in Null @ γ' | Link P γ']))%I.
       iApply (GPS_PP_Read (p:=γ) (Link P γ) True%I Q' with "kI [$os]");
         [done|done|..].
-      { iNext. iSplitL.
+      { iSplitL.
         - iIntros (s'). iIntros "_". iLeft.
-          iIntros (n). iIntros "(LinkInt & _)".
+          iIntros (n). iIntros "!> (LinkInt & _)".
           rewrite (unf_int (Link P)).
           iModIntro. iIntros "%".
           destruct s' as [|l'].
@@ -407,7 +406,7 @@ Section MSQueue.
             rewrite (_: Z.to_pos (Z.pos l' + 1) = ZplusPos 1 l'); last first.
             { rewrite /ZplusPos. f_equal. omega. }
             iFrame "DEQ Link".
-        - rewrite /monPred_absolutely /=. iIntros (????) "_ [_ #$] //". }
+        - rewrite monPred_absolutely_unfold /=. iIntros "!>" (????) "_ [_ #$] //". }
 
       iNext. iIntros (s' n) "(_ & #os & Q')".
       wp_seq. wp_op. case_bool_decide.
@@ -422,7 +421,8 @@ Section MSQueue.
         iApply (GPS_PP_CAS (p:=()) (Head P) True%I Q1 (λ _ _, True)%I
                   with "kI []"); [done|done|..].
         { iSplitL; last iSplitL; last first.
-          - rewrite /monPred_absolutely /=. iIntros "{$oH} !>" (?????) "[_ #$] //".
+          - rewrite monPred_absolutely_unfold /=.
+            iIntros "{$oH} !>" (?????) "[_ #$] //".
           - iNext. by iIntros (??) "_".
           - iNext. iIntros ([]).
             iIntros "(_ & Head & _)".
@@ -440,7 +440,7 @@ Section MSQueue.
             iModIntro. iExists (). iSplitL ""; first auto.
             iSplitL "od P".
             + iExists x. iFrame "od P".
-            + iNext. iSplitL "Tok".
+            + iSplitL "Tok".
               * iExists γ'. iFrame "on Tok".
               * iSplitL; first done. iExists γ'. iFrame "on". }
 
diff --git a/theories/examples/spin_lock.v b/theories/examples/spin_lock.v
index f7cf459d92c79f5b381e42171c3276d4e68e9da4..019fb72cef820492ea4c7a1da4d3313ff1ec58d0 100644
--- a/theories/examples/spin_lock.v
+++ b/theories/examples/spin_lock.v
@@ -33,7 +33,7 @@ Section proof.
   Notation Q_dup := (λ v, (v = 1) ∨ (v = 0)).
   Notation Q J := (λ v, (v = 1) ∨ (v = 0 ∧ J)).
   Instance Frame_Into_Q (J : vPred) v :
-    ∀ V, KnownFrame false (J V) (Q J v V) (Q_dup v V)%V.
+    ∀ V, Frame false (J V) (Q J v V) (Q_dup v V)%V.
   Proof. iIntros (V) "[oJ [%|%]]"; [by iLeft|iRight]. by iFrame "oJ". Qed.
 
   Definition isLock (l : loc) J : vPred :=
diff --git a/theories/examples/ticket_lock.v b/theories/examples/ticket_lock.v
index a93496522eb2cfc52c6a37ff33bc514ace35b87f..a0b674a58ee38efcc199770efcce9bccdfa6b689 100644
--- a/theories/examples/ticket_lock.v
+++ b/theories/examples/ticket_lock.v
@@ -352,7 +352,7 @@ Section TicketLock.
 
     Lemma Perm_exclusive γ t: Perm γ t ∗ Perm γ t ⊢ False.
     Proof.
-      rewrite /Perms /Perm -bi_embed_sep -own_op pair_op.
+      rewrite /Perms /Perm -embed_sep -own_op pair_op.
       iIntros "Perms".
       iDestruct (own_valid with "Perms") as %[Valid _]. exfalso.
       simpl in Valid.
@@ -363,7 +363,7 @@ Section TicketLock.
     Lemma Perms_get γ t :
       Perms γ t ⊢ Perm γ t ∗ Perms γ (S t).
     Proof.
-      rewrite /Perms /Perm -bi_embed_sep -own_op pair_op.
+      rewrite /Perms /Perm -embed_sep -own_op pair_op.
       iIntros "Perms".
       (* iSplitL. *)  (* TODO: why is this slow? *)
       rewrite !/op /cmra_op /=.
@@ -385,7 +385,7 @@ Section TicketLock.
     Lemma MyAll_coherent γ i t M:
       AllTkts γ M ∗ MyTkt γ i t ⊢ ⌜M !! i = Excl' t⌝.
     Proof.
-      rewrite /Perms /Perm -bi_embed_sep -own_op pair_op.
+      rewrite /Perms /Perm -embed_sep -own_op pair_op.
       iIntros "Perms".
       iDestruct (own_valid with "Perms") as %[_ Valid].
       iPureIntro.
@@ -403,7 +403,7 @@ Section TicketLock.
     Proof.
       iIntros "Own".
       iDestruct (MyAll_coherent with "Own") as %Eq.
-      rewrite /AllTkts -bi_embed_sep -!own_op !pair_op.
+      rewrite /AllTkts -embed_sep -!own_op !pair_op.
       iMod (own_update with "Own") as "[$ $]"; [|done].
       apply prod_update; [done|].
       apply auth_update.
@@ -566,7 +566,7 @@ Section TicketLock.
       iApply (GPS_PP_Init_default (TCP P γ x) ()
                 with "[$kI $kP] [$oTC Perms AllTkts NSR]");
                 [done|done| |].
-      { iNext. iSplitR ""; last done.
+      { iSplitR ""; last done.
         iExists O, O, firstMap. iFrame "AllTkts Perms NSR".
         iPureIntro. split; last split.
         + rewrite /firstMap /map_excl. apply set_unfold_2. move => i.
@@ -622,7 +622,7 @@ Section TicketLock.
           destruct ot as [t0|]; first (move: (nEq2 t0) => [//|->|-> //]).
           + by iApply ("NS" $! t0 with "[%]").
           + by rewrite nEq1.
-        - iModIntro. iNext. iSplitR ""; last done.
+        - iModIntro. iSplitR ""; last done.
           iExists (S t), n', (<[i := Excl (Some t)]> M).
           iFrame "All' Perms". iSplitR "NSR".
           + iPureIntro. split; last split.
@@ -655,7 +655,7 @@ Section TicketLock.
           rewrite !(unf_int (NSP P γ)).
           by iDestruct "NSP" as "($ & $)".
         - (* TODO : make iAlways able to introduce monPred_absolutely here. *)
-          rewrite /monPred_absolutely /=. iIntros (?????) "!> (? & #$) //". }
+          rewrite monPred_absolutely_unfold. iIntros (?????) "!> (? & #$) //". }
 
       iNext. iIntros (n z) "(% & #NSR & Q2)".
       iDestruct "Q2" as "(% & #ES)".
@@ -726,7 +726,7 @@ Section TicketLock.
       wp_lam. wp_bind ([_]_at)%E. wp_op.
 
       iApply (GPS_SW_Read_ex (NSP P γ) with "[$kI $NSW]"); [done|done|..].
-      { rewrite /monPred_absolutely /=. iIntros "!>" (????) "#$ //". }
+      { rewrite monPred_absolutely_unfold. iIntros "!>" (????) "#$ //". }
 
       iNext. iIntros (z) "(NSW & NSP)".
       rewrite (unf_int (NSP P γ)).
diff --git a/theories/examples/tstack.v b/theories/examples/tstack.v
index 6926c86f896fa81b524e562caae5639688fc7303..987760270239d0e3934ba80274e7ba3b25be6597 100644
--- a/theories/examples/tstack.v
+++ b/theories/examples/tstack.v
@@ -175,7 +175,7 @@ Section TreiberStack.
       wp_seq. wp_bind ([_]_na <- _)%E.
       iApply (GPS_PP_Init_default (Head P) () with "[$kI $kP] [$os]");
         [done|done|..].
-      { iNext; iSplitL; iExists [].
+      { iSplitL; iExists [].
         - by rewrite /Reachable (fixpoint_unfold (Reachable' P) _ _).
         - by rewrite /ReachableD (fixpoint_unfold (ReachableD') _ _). }
       iNext. iIntros "Head".
@@ -204,10 +204,10 @@ Section TreiberStack.
       iApply (GPS_PP_Read (p := ()) (Head P) True%I (λ _ _, True)%I
           with "kI [$Stack]");
         [done|done|..].
-      { iNext. iSplitL.
-        - iIntros (?) "_". iLeft. by iIntros (?) "_".
-        - rewrite /monPred_absolutely /tc_opaque. setoid_rewrite <-Head_dup.
-          by iIntros (?????) "[_ $]". }
+      { iSplitL.
+        - iIntros (?) "_". iLeft. by iIntros "!>" (?) "_".
+        - rewrite monPred_absolutely_unfold. setoid_rewrite <-Head_dup.
+          by iIntros "!>" (?????) "[_ $]". }
 
       iNext. iIntros ([] h) "(_ & Head & _)".
       wp_seq. wp_bind ([_]_na <- _)%E. wp_op.
@@ -221,7 +221,7 @@ Section TreiberStack.
       { iSplitL ""; last iSplitL ""; last iSplitL "".
         - iNext. iIntros ([]) "(_ & Head & P & od & ol)".
           iExists (). do 2 (iSplitL ""; first done).
-          iModIntro. iNext. iApply Head_dup_main.
+          iModIntro. rewrite -bi.later_sep. iApply Head_dup_main.
           iDestruct "Head" as (A) "Head".
           iExists (x :: A).
           rewrite /Reachable !(fixpoint_unfold (Reachable' P) _ _).
@@ -232,7 +232,7 @@ Section TreiberStack.
           + iExists _, _. iFrame "ol". iNext.
             by rewrite /Reachable' (fixpoint_unfold (Reachable' P) _ _).
         - iNext. by iIntros (??) "(_ & _ & _ & ?)".
-        - rewrite /monPred_absolutely /tc_opaque. setoid_rewrite <-Head_dup.
+        - rewrite monPred_absolutely_unfold. setoid_rewrite <-Head_dup.
           iIntros (?????) "!> [_ $] //".
         - by iFrame. }
 
@@ -255,8 +255,8 @@ Section TreiberStack.
                 ⌜0 < h⌝%Z ∗ ∃ q n, (Z.to_pos (h + next)) ↦{q} n)%I.
       iApply (GPS_PP_Read (p := ()) (Head P) True%I Q with "kI [$Stack]");
         [done|done|..].
-      { iNext. iSplitL.
-        - iIntros (?) "_". iLeft. iIntros (h) "[Head _]".
+      { iSplitL.
+        - iIntros (?) "_". iLeft. iIntros "!>" (h) "[Head _]".
           iDestruct "Head" as (A) "Head".
           iModIntro. iIntros "%".
           rewrite /ReachableD (fixpoint_unfold (ReachableD') _ _).
@@ -264,8 +264,8 @@ Section TreiberStack.
           + by iDestruct "Head" as "%".
           + iDestruct "Head" as "[$ Head]".
             iDestruct "Head" as (q) "[Head _]". by iExists _, _.
-        - rewrite /monPred_absolutely /tc_opaque. setoid_rewrite <- Head_dup.
-          iIntros (?????) "[_ $] //". }
+        - rewrite monPred_absolutely_unfold. setoid_rewrite <- Head_dup.
+          iIntros "!>" (?????) "[_ $] //". }
 
       iNext. iIntros ([] h) "(_ & Head & Q)".
       wp_seq. wp_op.
@@ -288,8 +288,8 @@ Section TreiberStack.
           λ _, (∃ v, (ZplusPos data (Z.to_pos h)) ↦ v ∗ P v)%I.
         iApply (GPS_PP_CAS (p := ()) (Head P) P' Q' (λ _ _, True)%I
                 with "kI [$oh $Head]"); [done|done|..].
-        { iNext. iSplitL; last iSplitL.
-          - iIntros ([]) "(_ & Head & oh)".
+        { iSplitL; last iSplitL.
+          - iIntros "!>" ([]) "(_ & Head & oh)".
             iExists (). iSplitL ""; first done.
             iDestruct "Head" as (A) "Head".
             rewrite /Reachable (fixpoint_unfold (Reachable' P) _ _).
@@ -308,12 +308,12 @@ Section TreiberStack.
                 rewrite (_: ZplusPos 1 (Z.to_pos h) = Z.to_pos (h + 1));
                   first done.
                 rewrite /ZplusPos. f_equal. rewrite Z2Pos.id; [omega|done].
-              * iNext. iApply Head_dup_main.
+              * rewrite -bi.later_sep. iNext. iApply Head_dup_main.
                 iExists A'.
                 by rewrite /Reachable (fixpoint_unfold (Reachable' P) _ _).
-          - by iIntros.
-          - rewrite /monPred_absolutely /tc_opaque. setoid_rewrite <- Head_dup.
-            iIntros (?????) "[_ $] //". }
+          - iNext. by iIntros.
+          - rewrite monPred_absolutely_unfold. setoid_rewrite <- Head_dup.
+            iIntros "!>" (?????) "[_ $] //". }
 
         iNext. iIntros ([] [] _) "(_ & Head & IF)".
         + wp_if_true.
diff --git a/theories/examples/unit_token.v b/theories/examples/unit_token.v
index feb687cfaeed9f301253b14647b59f551fe07ddc..d2e53e461641c4e6d997fe3679ffd0958e2acbd6 100644
--- a/theories/examples/unit_token.v
+++ b/theories/examples/unit_token.v
@@ -19,7 +19,7 @@ Section UnitToken.
 
   Lemma unit_tok_exclusive γ: iTok γ ∗ iTok γ ⊢ False.
   Proof.
-    iIntros "excl". rewrite -bi_embed_sep -own_op.
+    iIntros "excl". rewrite -embed_sep -own_op.
     iDestruct (own_valid with "excl") as %Valid.
     by apply (excl_exclusive (Excl ())) in Valid.
   Qed.
diff --git a/theories/gps/fractional.v b/theories/gps/fractional.v
index a3ff8cd6242ec52eb0e12855a57d52d41b272f2a..91c616ef11e79d1a8bdd8f7255b7003f58a40bfd 100644
--- a/theories/gps/fractional.v
+++ b/theories/gps/fractional.v
@@ -216,15 +216,15 @@ Section Fractional.
     subst X. apply encode_inj in H1. inversion H1. subst γ' γ_x'.
 
     rewrite monPred_in_eq /=.
-    iDestruct "RA" as (V_r v_r) "(% & % & #oR)".
+     iDestruct "RA" as (V_r v_r) "(% & % & #oR)".
 
     iApply (RawProto_Read IP l P (fun s v => |={E ∖ ↑fracN .@ l, E}=> Q s v)%I _ _ _ V_r v_r γ γ_x
             with "[VS $oI $kI $kS $oP $oR VSDup Writer Hex HClose]");
       [solve_ndisj|solve_jsl|..].
-    { iNext. iSplitR "VSDup"; last by iSpecialize ("VSDup" $! _).
+    { iSplitR "VSDup"; last by iSpecialize ("VSDup" $! _).
       iIntros (s' j ? Hs').
       iDestruct ("VS" $! _ j with "[%] [%//]") as "[VS|VS]"; [solve_jsl| |by iRight].
-      iLeft; iIntros (v Vr j0 Hle') "(? & ? & % & % & oI & oR')".
+      iLeft; iIntros "!>" (v Vr j0 Hle') "(? & ? & % & % & oI & oR')".
       iMod ("HClose" $! (RFRaw s V) with "[Writer oI oR' Hex]").
       { iSplitL "oI Writer".
         + iNext. iExists γ, γ_x, ζ. iFrame; auto.
@@ -302,7 +302,7 @@ Section Fractional.
     iMod ("VS" $! _ with "[%] [oP oW]") as "($ & oF & oFp)"; first done.
     { rewrite vGPS_FP_eq /=; iFrame. }
     iSpecialize ("oI" with "[$oF $oFp]").
-    iMod ("HClose" with "[-]") as "$".
+    iMod ("HClose" with "[-]") as "$"; [|done].
     iNext. iExists γ, γ_x, ({[s', (v, V')]} ∪ ζ).
     iFrame "wTok". by iSplit.
   Qed.
@@ -457,15 +457,15 @@ Section Fractional.
     intros; iIntros "#kI !#" (?) "(VS & VSF & VSDup & oP & oW) Post".
     iApply (GPS_FP_CAS' _ _ _ _ _ _ P (fun s => vGPS_FP l s q ∗ Q s)%I
       (fun s v => vGPS_FP l s q ∗ R s v)%I with "[$kI VS VSF $VSDup $oP $oW]");
-      [done | done | .. |]; iNext.
+      [done | done | .. |].
     { iSplitL "VS".
-      - iIntros (?) "Hs'"; iMod ("VS" with "Hs'") as (s'') "(? & ? & ? & ?)".
+      - iIntros "!>" (?) "Hs'"; iMod ("VS" with "Hs'") as (s'') "(? & ? & ? & ?)".
         iExists s''; iFrame.
         iModIntro; auto.
-      - iIntros (??) "(? & ? & ? & ? & ?)"; iFrame.
+      - iIntros "!>" (??) "(? & ? & ? & ? & ?)"; iFrame.
         iApply fupd_mask_mono; last by iApply "VSF"; iFrame.
         solve_ndisj. }
-    iIntros (s'' b v) "(? & ?)".
+    iIntros "!>" (s'' b v) "(? & ?)".
     destruct b; iApply ("Post" $! s'' _ v); iFrame.
   Qed.
 
diff --git a/theories/gps/plain.v b/theories/gps/plain.v
index b681c07fc09b9c119c6429f81b05fbb22b51ac97..0bc606bb7d0661bf0205d9bb0509b73f700bb0ac 100644
--- a/theories/gps/plain.v
+++ b/theories/gps/plain.v
@@ -62,10 +62,10 @@ Section Plain.
   Qed.
 
   Local Instance :
-    KnownFrame false (gps_inv IP l γ γ_x) (gpsPRaw p l (encode (p,γ,γ_x,γx)))
-               (Writer γ ζ ∗ exwr γ_x 1%Qp e_x ∗ own.own γx (DecAgree e_x)).
+    Frame false (gps_inv IP l γ γ_x) (gpsPRaw p l (encode (p,γ,γ_x,γx)))
+          (Writer γ ζ ∗ exwr γ_x 1%Qp e_x ∗ own.own γx (DecAgree e_x)).
   Proof.
-    intros. rewrite /KnownFrame /Frame. iIntros "[? ?]". iExists _, _.
+    intros. rewrite /Frame. iIntros "[? ?]". iExists _, _.
     iFrame "∗". iExists _, _, _. cbn. by iFrame "∗".
   Qed.
 
@@ -349,15 +349,15 @@ Section Plain.
     intros; iIntros "#kI !#" (?) "(VS & VSF & VSDup & oP & oW) Post".
     iApply (GPS_PP_CAS' _ _ _ _ _ _ P (fun s => vGPS_PP l p s ∗ Q s)%I
       (fun s v => vGPS_PP l p s ∗ R s v)%I with "[$kI VS VSF $VSDup $oP $oW]");
-      [done | done | .. |]; iNext.
+      [done | done | .. |].
     { iSplitL "VS".
-      - iIntros (?) "Hs'"; iMod ("VS" with "Hs'") as (s'') "(? & ? & ? & ?)".
+      - iIntros "!>" (?) "Hs'"; iMod ("VS" with "Hs'") as (s'') "(? & ? & ? & ?)".
         iExists s''; iFrame.
         iModIntro; auto.
-      - iIntros (??) "(? & ? & ? & ? & ?)"; iFrame.
+      - iIntros "!>" (??) "(? & ? & ? & ? & ?)"; iFrame.
         iApply fupd_mask_mono; last by iApply "VSF"; iFrame.
         solve_ndisj. }
-    iIntros (s'' b v) "(? & ?)".
+    iIntros "!>" (s'' b v) "(? & ?)".
     destruct b; iApply ("Post" $! s'' _ v); iFrame.
   Qed.
 
diff --git a/theories/gps/singlewriter.v b/theories/gps/singlewriter.v
index 2eb60a74bafabe970fd4c1f02fa1ff2667be5303..517f21e7102f0793fb8df897b1da4161f860f34a 100644
--- a/theories/gps/singlewriter.v
+++ b/theories/gps/singlewriter.v
@@ -72,11 +72,9 @@ Section Gname_StrongSW.
   Close Scope I.
 
   Local Instance :
-    KnownFrame false (gps_inv (IP γ) l γ γ_x)
+    Frame false (gps_inv (IP γ) l γ γ_x)
           (gpsSWnRaw γ l (encode (γ, (γ_x)))) True.
-  Proof.
-    intros. rewrite /KnownFrame /Frame /=. iIntros "[? _]". iExists _. by iFrame "∗".
-  Qed.
+  Proof. intros. rewrite /Frame /=. iIntros "[? _]". iExists _. by iFrame "∗". Qed.
 
   Lemma GPS_nFWP_Init_strong l (s: gname -> pr_state Prtcl) v
     (Q : gname -> vPred) (E : coPset) (HEN : ↑physN ⊆ E):
@@ -405,8 +403,8 @@ Section Gname_StrongSW.
 
     iApply (RawProto_Read (IP γ) l P (fun s v => |={E ∖ ↑fracN.@l, E}=> Q s v)%I s _ _ V_r v_r γ γ_x
             with "[VS $oI $kI $kS $oP $oR VSDup HClose]"); [solve_ndisj|auto|..].
-    { iNext; iSplitR "VSDup"; last by iSpecialize ("VSDup" $! _).
-      iIntros (s' j ?) "Hs'".
+    { iSplitR "VSDup"; last by iSpecialize ("VSDup" $! _).
+      iIntros "!>" (s' j ?) "Hs'".
       iDestruct ("VS" $! _ j with "[//] [Hs' //]") as "[VS|VS]"; last by iRight.
       iLeft; iIntros (v Vr j0 Hle') "(? & ? & % & % & oI & oR')".
       iMod ("HClose" $! (fun l _ p => ReaderSWnRaw γ s' j0 l p) with "[oI oR']").
@@ -473,11 +471,11 @@ Section Gname_StrongSW.
     destruct H2 as [Hs2|Hs1].
     - iApply (RawProto_Read (IP γ) l P (fun s v => |={E ∖ ↑fracN .@ l, E}=> Q s v)%I s2 _ _ V2 v2 γ γ_x
                 with "[$oI $kI $kS $oP $oR2 VS VSDup HClose]"); [solve_ndisj|solve_jsl|..].
-      { iNext. iSplitR "VSDup".
+      { iSplitR "VSDup".
         - iIntros (s' j ??).
           iDestruct ("VS" $! _ _ with "[%] [%]") as "[VS|VS]"; last by iRight.
           { solve_jsl. } { split; solve_jsl. }
-          iLeft; iIntros (v Vr j0 Hle') "(? & ? & % & % & oI & oR')".
+          iLeft; iIntros "!>" (v Vr j0 Hle') "(? & ? & % & % & oI & oR')".
           iMod ("HClose" $! (fun l _ => ReaderSWnRaw γ s1 V l) with "[oI oR']").
           { iSplitL "oI".
             + iNext. iExists γ_x. iFrame; auto.
@@ -485,7 +483,7 @@ Section Gname_StrongSW.
           iMod ("VS" $! _ _ with "[%] [-]") as "$"; first done.
           { iFrame. }
           iApply fupd_intro_mask'. solve_ndisj.
-        - iIntros (s' v ??) "[% Fp]".
+        - iIntros "!>" (s' v ??) "[% Fp]".
           iApply ("VSDup" $! _ s' v _ with "[%] [$Fp]"); first reflexivity.
           iPureIntro. split; [by etrans|auto]. }
       iNext. iIntros (s' v Vr V'') "(% & kS & % & Q & oR' & % & %)".
@@ -494,11 +492,11 @@ Section Gname_StrongSW.
       iPureIntro; split; [by etrans|auto].
     - iApply (RawProto_Read (IP γ) l P (fun s v => |={E ∖ ↑fracN .@ l, E}=> Q s v)%I s1 _ _ V1 v1 γ γ_x
                 with "[$oI $kI $kS $oP $oR1 VS VSDup HClose]"); [solve_ndisj|solve_jsl|..].
-      { iNext. iSplitR "VSDup".
+      { iSplitR "VSDup".
         - iIntros (s' j ??).
           iDestruct ("VS" $! _ _ with "[%] [%]") as "[VS|VS]"; last by iRight.
           { solve_jsl. } { split; solve_jsl. }
-          iLeft; iIntros (v Vr j0 Hle') "(? & ? & % & % & oI & oR')".
+          iNext. iLeft; iIntros (v Vr j0 Hle') "(? & ? & % & % & oI & oR')".
           iMod ("HClose" $! (fun l _ => ReaderSWnRaw γ s1 V l) with "[oI oR']").
           { iSplitL "oI".
             + iNext. iExists γ_x. iFrame; auto.
@@ -506,7 +504,7 @@ Section Gname_StrongSW.
           iMod ("VS" $! _ _ with "[%] [-]") as "$"; first done.
           { iFrame. }
           iApply fupd_intro_mask'. solve_ndisj.
-        - iIntros (s' v ??) "[% Fp]".
+        - iIntros "!>" (s' v ??) "[% Fp]".
           iApply ("VSDup" $! _ s' v _ with "[%] [$Fp]"); first reflexivity.
           iPureIntro. split; solve_jsl. }
       iNext. iIntros (s' v Vr V'') "(% & kS & % & Q & oR' & % & %)".
@@ -565,11 +563,11 @@ Section Gname_StrongSW.
     iApply (RawProto_Read (IP γ) l P (fun s v => |={E ∖ ↑fracN .@ l, E}=> Q s v)%I s _ _ V1 v1 γ γ_x
                 with "[$oI $kI $kS $oP $oR VS VSDup HClose]"); [solve_ndisj|auto|..].
     { solve_jsl. }
-    { iNext. iSplitR "VSDup"; last by iSpecialize ("VSDup" $! _).
+    { iSplitR "VSDup"; last by iSpecialize ("VSDup" $! _).
       iIntros (s' j ??).
       iDestruct ("VS" $! _ _ with "[%] [//]") as "[VS|VS]"; last by iRight.
       { solve_jsl. }
-      iLeft; iIntros (v Vr j0 Hle') "(? & ? & % & % & oI & oR')".
+      iLeft; iIntros "!>"(v Vr j0 Hle') "(? & ? & % & % & oI & oR')".
       iMod ("HClose" $! (fun l _ => ReaderSWnRaw γ s V l) with "[oI oR']").
       { iSplitL "oI".
         + iNext. iExists γ_x. iFrame; auto.
@@ -822,11 +820,11 @@ Section Gname_StrongSW_Param.
     iApply (RawProto_Read (IP γ) l P (fun s v => |={E ∖ ↑persist_locN.@l, E}=> Q s v)%I s _ _ V_r v_r γ γ_x
               with "[VS $oI $kI $kS $oP $oR VSDup HClose]"); [solve_ndisj|auto|..].
     { etrans; eauto. }
-    { iNext; iSplitR "VSDup"; last by iSpecialize ("VSDup" $! _).
+    { iSplitR "VSDup"; last by iSpecialize ("VSDup" $! _).
       iIntros (s' j ? Hs').
       iDestruct ("VS" $! _ Hs' j with "[%]") as "[VS|VS]"; last by iRight.
       { etrans; eauto. }
-      iLeft; iIntros (v Vr j0 Hle') "(? & ? & % & % & oI & oR')".
+      iLeft; iIntros "!>" (v Vr j0 Hle') "(? & ? & % & % & oI & oR')".
       iMod ("HClose" $! (λ l X, ReaderSWpnRaw p γ s' l X j0) with "[oI oR']").
       { iSplit.
         + iNext. iExists γ_x. by iFrame "oI".
@@ -1024,9 +1022,9 @@ Section SingleWriter.
   Definition vGPS_FWP_eq : vGPS_FWP = _ := seal_eq _.
 
   Local Instance :
-    KnownFrame false (gps_inv IP l γ γ_x) (gpsSWRaw l (encode (γ, (γ_x)))) True.
+    Frame false (gps_inv IP l γ γ_x) (gpsSWRaw l (encode (γ, (γ_x)))) True.
   Proof.
-    intros. unfold KnownFrame, Frame, bi_affinely_if, bi_persistently_if.
+    intros. unfold Frame, bi_affinely_if, bi_persistently_if.
     iIntros "[H _]". iExists _, _. by iFrame "∗".
   Qed.
   Local Close Scope I.
@@ -1184,11 +1182,11 @@ Section SingleWriter.
     iApply (RawProto_Read IP l P (fun s v => |={E ∖ ↑persist_locN.@l, E}=> Q s v)%I s _ _ V_r v_r γ γ_x
               with "[VS $oI $kI $kS $oP $oR VSDup HClose]"); [solve_ndisj|auto|..].
     { etrans; eauto. }
-    { iNext; iSplitR "VSDup"; last by iSpecialize ("VSDup" $! _).
+    { iSplitR "VSDup"; last by iSpecialize ("VSDup" $! _).
       iIntros (s' j ? Hs').
       iDestruct ("VS" $! _ Hs' j with "[%]") as "[VS|VS]"; last by iRight.
       { etrans; eauto. }
-      iLeft; iIntros (v Vr j0 Hle') "(? & ? & % & % & oI & oR')".
+      iLeft; iIntros "!>" (v Vr j0 Hle') "(? & ? & % & % & oI & oR')".
       iMod ("HClose" $! (λ l X, ReaderSWRaw s' l X j0) with "[oI oR']").
       { iSplit.
         + iNext. iExists γ, γ_x. by iFrame "oI".
@@ -1366,11 +1364,11 @@ Section SingleWriter.
     iApply (RawProto_Read IP l P (fun s v => |={E ∖ ↑fracN.@l, E}=> Q s v)%I s _ _ V_r v_r γ γ_x
               with "[VS $oI $kI $kS $oP $oR VSDup HClose]"); [solve_ndisj|auto|..].
     { etrans; eauto. }
-    { iNext; iSplitR "VSDup"; last by iSpecialize ("VSDup" $! _).
+    { iSplitR "VSDup"; last by iSpecialize ("VSDup" $! _).
       iIntros (s' j ? Hs').
       iDestruct ("VS" $! _ Hs' j with "[%]") as "[VS|VS]"; last by iRight.
       { etrans; eauto. }
-      iLeft; iIntros (v Vr j0 Hle') "(? & ? & % & % & oI & oR')".
+      iLeft; iIntros "!>" (v Vr j0 Hle') "(? & ? & % & % & oI & oR')".
       iMod ("HClose" $! (fun l _ X => ReaderSWRaw s' l X j0) with "[oI oR']").
       { iSplit.
         + iNext. iExists γ, γ_x. by iFrame "oI".
diff --git a/theories/invariants.v b/theories/invariants.v
index 93360826ec322875256a63c7d5f3ce81360899c0..fb5cc9b168c15aaf3db50982f7667e4f7826f475 100644
--- a/theories/invariants.v
+++ b/theories/invariants.v
@@ -9,14 +9,14 @@ Section Invariants.
 
   Lemma inv_alloc N (E : coPset) (P : vProp Σ) : ▷ (∀ᵢ P) -∗ |={E}=> inv N P.
   Proof.
-    iIntros "H". rewrite /monPred_absolutely /= -sbi_embed_later.
+    iIntros "H". rewrite monPred_absolutely_unfold /= -embed_later.
     by iMod (invariants.inv_alloc with "H") as "$".
   Qed.
 
   Lemma inv_alloc_open N (E : coPset) (P : vProp Σ) :
     ↑N ⊆ E → (|={E,E ∖ ↑N}=> inv N P ∗ (▷ (∀ᵢ P) ={E ∖ ↑N,E}=∗ True))%I.
   Proof.
-    rewrite /monPred_absolutely /= -sbi_embed_later.
+    rewrite monPred_absolutely_unfold /= -embed_later.
     iIntros (?). iMod (invariants.inv_alloc_open) as "[$ Close]"; [done|].
     iIntros "!> H". by iMod ("Close" with "H").
   Qed.
@@ -24,7 +24,7 @@ Section Invariants.
  Lemma inv_open (E : coPset) N (P : vProp Σ) :
    ↑N ⊆ E → inv N P -∗ |={E,E ∖ ↑N}=> ▷ (∀ᵢ P) ∗ (▷ (∀ᵢ P) ={E ∖ ↑N,E}=∗ True).
  Proof.
-   iIntros (?) "H". rewrite /monPred_absolutely /= -sbi_embed_later.
+   iIntros (?) "H". rewrite monPred_absolutely_unfold /= -embed_later.
    iMod (invariants.inv_open with "H") as "[$ Close]"; [done|].
    iIntros "!> H". by iMod ("Close" with "H").
  Qed.
diff --git a/theories/iris_lemmas.v b/theories/iris_lemmas.v
index a1825faec244650c45fe33efaa764f6c33211355..fea8499b95edd94e70c922e5c4a42d824ea94def 100644
--- a/theories/iris_lemmas.v
+++ b/theories/iris_lemmas.v
@@ -25,7 +25,7 @@ Section Extra.
     : ▷ (φ s -∗ φ s ∗ φ s) ∗ ▷ ([∗ set] s' ∈ S, φ s')
       ⊢ ▷ φ s ∗ ▷ ([∗ set] s' ∈ S, φ s').
   Proof.
-    iIntros "(Dup & ress)". iNext.
+    iIntros "(Dup & ress)". rewrite -bi.later_sep. iNext.
     by iApply (big_sepS_dup with "[$Dup $ress]").
   Qed.
 
diff --git a/theories/na.v b/theories/na.v
index 1e6138ed8e784c8e7975dbc7ec61d2e8edc87492..b682fc4050184d6607fe2aa12f20a5de36820f99 100644
--- a/theories/na.v
+++ b/theories/na.v
@@ -57,9 +57,9 @@ Section Exclusive.
   (* Proof. apply _. Qed. *)
 
   Global Instance Frame_na_ownloc l v:
-    KnownFrame false ((own_loc_na l v)) (own_loc l) (True%I) | 1.
+    Frame false ((own_loc_na l v)) (own_loc l) (True%I) | 1.
   Proof.
-    rewrite /own_loc_na /own_loc /KnownFrame /Frame. iStartProof (uPred _).
+    rewrite /own_loc_na /own_loc /Frame. iStartProof (uPred _).
     iIntros (?) "[H _] /=". iDestruct "H" as (?) "?". iExists _. eauto.
   Qed.
 
diff --git a/theories/proofmode.v b/theories/proofmode.v
index d1ec1415e69ee253c94533f62a6e71ef90cd1b4c..b73a0f93a9766375bbbe0d8e65e848f67847cba3 100644
--- a/theories/proofmode.v
+++ b/theories/proofmode.v
@@ -2,11 +2,8 @@ From iris.proofmode Require Export tactics.
 From igps Require Import viewpred.
 
 Global Instance Frame_vPred Σ p (P : vProp Σ) :
-  KnownFrame p (monPred_at P V) (monPred_at P V') ⌜V ⊑ V'⌝ | 30.
-Proof.
-  intros. unfold KnownFrame, Frame. iIntros "[? %]".
-  rewrite H. by destruct p => /=.
-Qed.
+  Frame p (monPred_at P V) (monPred_at P V') ⌜V ⊑ V'⌝ | 30.
+Proof. intros. unfold Frame. iIntros "[? %]". rewrite H. by destruct p => /=. Qed.
 Hint Extern 10 (IsBiIndexRel _ _) => unfold IsBiIndexRel; solve_jsl
             : typeclass_instances.
 
diff --git a/theories/rsl.v b/theories/rsl.v
index 89a49b8df0e261077fd93c27bf66ea6024414e0e..592ad208b15c7a121eca345e3365fb3a0c580fa4 100644
--- a/theories/rsl.v
+++ b/theories/rsl.v
@@ -220,7 +220,7 @@ Instance InitRaw_persistent V jγ : Persistent (InitRaw V jγ) := _.
     iDestruct ("SConv" $! v2 V2 with "HφR") as "HφR".
     rewrite (big_sepS_fn_insert (λ _ (f: Z → View → iProp), f v2 V2));
       last first.
-      { by move => /elem_of_difference [? _]. }
+    { by move => /elem_of_difference [? _]. }
     rewrite (big_sepS_delete _ _ _ In).
     iDestruct "HφR" as "(? & ?)". iFrame.
     case (decide (v = v2)) => [->|?].
@@ -291,7 +291,7 @@ Instance InitRaw_persistent V jγ : Persistent (InitRaw V jγ) := _.
           + iDestruct "ress" as (Ψ) "ress".
             iExists Ψ. iDestruct "ress" as "(#EConv & #Saved)".
             destruct H11 as [V'' EqV]. rewrite -EqV in H6.
-            iFrame "EConv Saved". iNext. iSplitL "Itpr".
+            iFrame "EConv Saved". iSplitL "Itpr".
             { iApply (big_sepS_subseteq _ ({[(VInj v, V');(A, V'')]}: History)).
               - by rewrite -H6.
               - rewrite big_sepS_insert; last by rewrite elem_of_singleton.
@@ -303,7 +303,7 @@ Instance InitRaw_persistent V jγ : Persistent (InitRaw V jγ) := _.
                 rewrite big_sepS_singleton. auto. }
           + iDestruct "ress" as (Ψ) "ress". (* TODO: duplicated proofs *)
             iExists Ψ. iDestruct "ress" as "[[#EConv #Saved] [ress ressD]]".
-            iFrame "EConv Saved". iNext.
+            iFrame "EConv Saved".
             pose p : Val * View := (VInj v, V').
             iSplitL "Itpr ress".
             * iApply (big_sepS_subseteq _  ({[VInj v, V']} ∪ h)); [by rewrite H6|].
@@ -319,19 +319,17 @@ Instance InitRaw_persistent V jγ : Persistent (InitRaw V jγ) := _.
           + iDestruct "ress" as (Ψ) "#ress2".
             destruct H11 as [V'' EqV]. rewrite -EqV in H6 .
             iSplitL "Itpr"; last iSplitL "ItprD".
-            { iNext.
-              iApply (big_sepS_subseteq _ ({[(VInj v, V');(A, V'')]}: History)).
+            { iApply (big_sepS_subseteq _ ({[(VInj v, V');(A, V'')]}: History)).
               * rewrite -H6. by apply subseteq_gset_filter.
               * rewrite big_sepS_insert; last by rewrite elem_of_singleton.
                 rewrite big_sepS_singleton. iSplitR ""; last done. by iApply "Conv". }
-            { iNext.
-              iApply (big_sepS_subseteq _ ({[(VInj v, V');(A, V'')]}: History)).
+            { iApply (big_sepS_subseteq _ ({[(VInj v, V');(A, V'')]}: History)).
               * by rewrite -H6.
               * rewrite big_sepS_insert; last by rewrite elem_of_singleton.
                 rewrite big_sepS_singleton. auto. }
             { iExists Ψ. iDestruct "ress2" as "(? & ?)". by iSplit. }
           + iDestruct "ress" as "(ress & ressD & ress2)". iFrame "ress2".
-            pose p : Val * View := (VInj v, V'). iNext.
+            pose p : Val * View := (VInj v, V').
             iSplitL "Itpr ress".
             { iApply (big_sepS_subseteq _  (gblock_ends l ({[VInj v, V']} ∪ h)));
                 [by rewrite H6|].
@@ -935,7 +933,7 @@ Instance InitRaw_persistent V jγ : Persistent (InitRaw V jγ) := _.
       + rewrite /RSLInv /sts_inv.
         iExists j, γ. iModIntro. iSplitL ""; first by iNext.
         iExists s'. iFrame "Own Hist' ress2".
-        iNext. iSplit; first auto. iNext. iSplitR "ressD"; last first.
+        iNext. iSplit; first auto. iSplitR "ressD"; last first.
         * iApply (big_sepS_subseteq _ _ h' with "[$ressD]").
           by rewrite H11 union_comm_L.
         * iApply (big_sepS_subseteq _ _ (gblock_ends l h') with "[$ress]").
diff --git a/theories/weakestpre.v b/theories/weakestpre.v
index 8ff3ed153b94621464b3f7391d1f35ab8c40508d..4af5c4a9420788b08d74fc0ce28270f272800d87 100644
--- a/theories/weakestpre.v
+++ b/theories/weakestpre.v
@@ -360,10 +360,8 @@ Section proofmode_classes.
 
   Global Instance frame_wp p E e R Φ Ψ :
     (∀ v, Frame p R (Φ v) (Ψ v)) →
-    KnownFrame p R (WP e @ E {{ Φ }}) (WP e @ E {{ Ψ }}).
-  Proof.
-    rewrite /KnownFrame /Frame=> HR. rewrite wp_frame_l. apply wp_mono, HR.
-  Qed.
+    Frame p R (WP e @ E {{ Φ }}) (WP e @ E {{ Ψ }}).
+  Proof. rewrite /Frame=> HR. rewrite wp_frame_l. apply wp_mono, HR. Qed.
 
   Global Instance is_except_0_wp E e Φ : IsExcept0 (WP e @ E {{ Φ }}).
   Proof. by rewrite /IsExcept0 -{2}fupd_wp -except_0_fupd -fupd_intro. Qed.