diff --git a/opam b/opam
index 83b7b9d2ba48c405e7b4cf9e5f67b0064c9ccb97..a960912f8382601c76747b474270064d379a6490 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-02-06.3") | (= "dev") }
+  "coq-iris" { (= "branch.gen_proofmode.2018-02-14.0") | (= "dev") }
 ]
diff --git a/theories/examples/circ_buffer.v b/theories/examples/circ_buffer.v
index 8bcf493d9414e84319943a4e5eee4740b160f706..024842a680e317b8fb72fc32740d016467e98521 100644
--- a/theories/examples/circ_buffer.v
+++ b/theories/examples/circ_buffer.v
@@ -164,8 +164,7 @@ Section CircBuffer.
       ([∗ list] i ∈ seq (Z.to_nat b) ni, (ZplusPos (Z.of_nat i) q) ↦ ?)%I
       ={↑escrowN}=∗ ([∗ list] i ∈ seq 0 ni, PE γ q i)%I.
     Proof.
-      move => Le. iIntros "OL".
-      iApply (fupd_big_sepL (PROP:=vProp _)).
+      move => Le. iIntros "OL". iApply fupd_big_sepL.
       rewrite (Nat2Z.id 2) -2!fmap_seq -list_fmap_compose bi.big_sepL_fmap.
       iApply (bi.big_sepL_mono with "OL").
       iIntros (? i H) "ol".
@@ -233,7 +232,7 @@ Section CircBuffer.
 
       iAssert (|={⊤}=> ([∗ list] i ∈ seq 0 (Z.to_nat n), PE γ q i)%I)%I
         with "[oLs]" as ">#PEs".
-      { iApply (fupd_mask_mono (PROP:=vProp) (↑escrowN)); first auto.
+      { iApply (fupd_mask_mono (↑escrowN)); first auto.
         iApply (cb_escrows_list_alloc with "oLs"). lia'. }
 
       wp_let. wp_op. wp_bind ([_]_na <- _)%E.
@@ -334,7 +333,7 @@ Section CircBuffer.
 
         iSpecialize ("EA" with "[$PEi $iTok]"); first auto.
 
-        iMod (fupd_mask_mono (PROP:=vProp) with "EA") as ">oL"; first auto.
+        iMod (fupd_mask_mono with "EA") as ">oL"; first auto.
 
         (* arithmetic *)
         rewrite (_: ZplusPos w (ZplusPos b q) = loc_at q i); last first.
@@ -347,7 +346,7 @@ Section CircBuffer.
         iDestruct (escrow_alloc ⎡cTok γ i⎤%I (∃ v : Z, P v ∗ loc_at q i ↦ v)%I with "[oL P]")
           as "CEi".
           { iNext. iExists v. iFrame "P oL". }
-        iMod (fupd_mask_mono (PROP:=vProp) with "CEi") as "#CEi"; first auto.
+        iMod (fupd_mask_mono with "CEi") as "#CEi"; first auto.
 
         wp_seq. wp_bind ([_]_at <- _)%E. wp_op.
         rewrite H0 Z.add_mod_idemp_l ; last omega.
@@ -363,8 +362,7 @@ Section CircBuffer.
             iSplitL ""; iIntros "!#"; [by rewrite Nat2Z.inj_add|].
             cbn. iIntros (k). iIntros (Hk).
             iApply ("Px"). iPureIntro. lia'.
-          - iIntros "!#". iIntros (k). iIntros "%".
-            apply Zlt_succ_le, Zle_lt_or_eq in a as [Lt|Eq].
+          - iIntros (k ?). apply Zlt_succ_le, Zle_lt_or_eq in a as [Lt|Eq].
             + by iApply ("CEs" with "[%]").
             + apply Nat2Z.inj in Eq. by rewrite Eq. }
 
@@ -432,7 +430,7 @@ Section CircBuffer.
           with "[] [$CEj $jTok]") as "EA".
         { iIntros "cTok". iApply (cTok_exclusive with "cTok"). }
 
-        iMod (fupd_mask_mono (PROP:=vProp) with "EA") as (v) "(P & >oL)"; [done|].
+        iMod (fupd_mask_mono with "EA") as (v) "(P & >oL)"; [done|].
 
         (* arithmetic *)
         rewrite (_: ZplusPos r (ZplusPos b q) = loc_at q j); last first.
@@ -452,7 +450,7 @@ Section CircBuffer.
             - rewrite /loc_at. do 2 f_equal.
               rewrite Nat2Z.inj_add Z2Nat.id; last omega.
               by rewrite -{1}(Z.mul_1_l n) Z_mod_plus_full. }
-        iMod (fupd_mask_mono (PROP:=vProp) with "PEj") as "#PEj"; first auto.
+        iMod (fupd_mask_mono with "PEj") as "#PEj"; first auto.
 
         wp_let. wp_bind ([_]_at <- _)%E. wp_op.
         wp_op. wp_op.
@@ -472,8 +470,7 @@ Section CircBuffer.
             iSplitL ""; iIntros "!#"; [by rewrite Nat2Z.inj_add|auto].
             cbn. iIntros (k). iIntros (Hk).
             iApply ("Px"). iPureIntro. lia'.
-          - iIntros "!#". iIntros (k). iIntros "%".
-            rewrite Z.add_succ_l in a.
+          - iIntros (k ?). rewrite Z.add_succ_l in a.
             apply Zlt_succ_le, Zle_lt_or_eq in a as [Lt|Eq].
             + by iApply ("PEs" with "[%]").
             + rewrite -(Nat2Z.id j) -Z2Nat.inj_add -?Eq ?Nat2Z.id;
diff --git a/theories/examples/hashtable.v b/theories/examples/hashtable.v
index c1b999deee55f994d4ed3a6bee48bfe9639fcb80..62023fe5dad5f33cfaf74dc04257b8c156ab9334 100644
--- a/theories/examples/hashtable.v
+++ b/theories/examples/hashtable.v
@@ -1967,7 +1967,7 @@ Section proof.
           destruct ls as [|b3]; [discriminate|].
           destruct ls; [|discriminate].
           iExists b1, b2, b3, h; simpl in *; iFrame; auto. }
-        iApply (fupd_mask_mono (PROP := vProp _) (↑escrowN)).
+        iApply (fupd_mask_mono (↑escrowN)).
         { apply namespaces.ndisj_subseteq_difference; last done.
           do 2 apply namespaces.ndot_preserve_disjoint_r.
           apply namespaces.ndot_ne_disjoint; done. }
@@ -2054,7 +2054,7 @@ Section proof.
     iPoseProof (big_sepL_mono with "Hentries") as "Hentries".
     { intros; iIntros "[Hctx H]".
       iApply (na_frac_from_non with "[$Hctx $H]"); auto. }
-    iMod (fupd_big_sepL (PROP:=vProp _) with "Hentries") as "Hentries".
+    iMod (fupd_big_sepL with "Hentries") as "Hentries".
     iApply (wp_for_simple with "[] [Hentries Ht Hhist Hresults]").
     { instantiate (1 := (fun i : Z => ⌜0 <= i <= 3⌝ ∗
         ([∗ list] j↦x ∈ entries, ZplusPos j m_entries ↦{1/Z.to_pos (2^i)} Z.pos x) ∗
@@ -2172,7 +2172,7 @@ Section proof.
           iPoseProof (escrow_apply with "[] [$H $Htok]") as "H".
           { iIntros "[H1 H2]".
            iPoseProof (own_valid_2 with "H1 H2") as "%"; done. }
-          iPoseProof (fupd_mask_mono (PROP:=vProp _)(↑escrowN) with "H") as ">H".
+          iPoseProof (fupd_mask_mono (↑escrowN) with "H") as ">H".
           { apply namespaces.ndisj_subseteq_difference; last done.
             do 2 apply namespaces.ndot_preserve_disjoint_r.
             apply namespaces.ndot_ne_disjoint; done. }
diff --git a/theories/examples/message_passing.v b/theories/examples/message_passing.v
index 73a986d6bea94495690242eaf3bc5faf0b347754..9dcc9ddd1a03d0fe4fd3eebbed5d9e0f56f855f8 100644
--- a/theories/examples/message_passing.v
+++ b/theories/examples/message_passing.v
@@ -107,8 +107,7 @@ Section proof.
           erewrite bool_decide_false; last auto.
           iSpecialize ("EA" with "[$XE $Tok]").
           iNext. iNext.
-          iApply fupd_wp.
-          iMod (fupd_mask_mono (PROP:=vProp _) with "EA") as "Nax"; [done|].
+          iApply fupd_wp. iMod (fupd_mask_mono with "EA") as "Nax"; [done|].
           iModIntro.
           wp_seq.
           iApply (na_read with "[$kI $Nax]"); [done|].
@@ -129,7 +128,7 @@ Section proof.
       (* allocate escrow *)
       iDestruct (escrow_alloc (Tok γ) (x ↦ 37)%I with "[$Nax]") as "XE".
 
-      iMod (fupd_mask_mono (PROP:=vProp _) _ ⊤ with "XE") as "XE"; first auto.
+      iMod (fupd_mask_mono _ ⊤ with "XE") as "XE"; first auto.
 
       (* write release to final state *)
       iApply (GPS_PP_Write (p:=()) (mpInt x γ) true (XE x γ) (λ _, True%I)
diff --git a/theories/examples/msqueue.v b/theories/examples/msqueue.v
index ce3b24713689db681badca56304f214cb13eecaa..d349367e55433e52455c818e8e6294323b1a918b 100644
--- a/theories/examples/msqueue.v
+++ b/theories/examples/msqueue.v
@@ -336,8 +336,7 @@ Section MSQueue.
                           (∃ v, ZplusPos data n ↦ v ∗ P v ∗ Tok γ'))%I as [EA].
               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 (PROP:=vProp _) with "DEQ") as "#DEQ";
-                first namespaces.solve_ndisj. (* TODO: make it work without (PROP:=..) *)
+              iMod (fupd_mask_mono with "DEQ") as "#DEQ"; first namespaces.solve_ndisj.
               iModIntro. iNext.
               rewrite !(unf_int (Link P)).
               iSplitL ""; (iSplitL ""; first done);
@@ -436,7 +435,7 @@ Section MSQueue.
                       with "[]") as "EA".
             { iIntros "[? ?]". iApply unit_tok_exclusive. iFrame. }
             iSpecialize ("EA" with "[$DEQ $Tok]").
-            iDestruct (fupd_mask_mono (PROP:=vProp _) with "EA") as "EA";
+            iDestruct (fupd_mask_mono with "EA") as "EA";
             [|iMod "EA" as (x) "(od & P & >Tok)"]; [namespaces.solve_ndisj|].
             iModIntro. iExists (). iSplitL ""; first auto.
             iSplitL "od P".
diff --git a/theories/examples/ticket_lock.v b/theories/examples/ticket_lock.v
index 87e2178bdf44905dbb99aa896c0e73da0ec44285..a93496522eb2cfc52c6a37ff33bc514ace35b87f 100644
--- a/theories/examples/ticket_lock.v
+++ b/theories/examples/ticket_lock.v
@@ -544,7 +544,7 @@ Section TicketLock.
         [done|done| |].
       { iIntros "oW".
         iDestruct (GPS_SW_Writer_Reader (IP := NSP P γ) with "oW") as "[oW $]".
-        iApply (fupd_mask_mono (PROP:=vProp _));
+        iApply fupd_mask_mono;
         last iMod (escrow_alloc (Perm γ 0)
                                 (P ∗ [XP ZplusPos 0 x in O |NSP P γ ]_W)%I
                      with "[$P $oW]") as "#?";
@@ -694,7 +694,7 @@ Section TicketLock.
             { by rewrite Perm_exclusive. }
 
             iSpecialize ("EA" with "[$ES $Perm]").
-            iMod (fupd_mask_mono (PROP:=vProp _) with "EA") as "(P & NSW)"; [done|].
+            iMod (fupd_mask_mono with "EA") as "(P & NSW)"; [done|].
             iDestruct (GPS_SW_Writer_max (IP := NSP P γ) x n t ⊤ with "[$NSR $NSW]") as ">(NSW & %)"; [done|].
               cbn in H3. exfalso. omega. }
 
@@ -703,7 +703,7 @@ Section TicketLock.
         iDestruct (escrow_apply (Perm γ n) (P ∗ [XP x in n | NSP P γ]_W)%I
               with "[] [$ES $Perm]") as "EA".
           { by rewrite Perm_exclusive. }
-        iMod (fupd_mask_mono (PROP:=vProp _) with "EA") as "(P & NSW)"; first auto.
+        iMod (fupd_mask_mono with "EA") as "(P & NSW)"; first auto.
         iDestruct (GPS_SW_Writer_max (IP := NSP P γ) x n n ⊤ with "[$NSR $NSW]") as ">(NSW & _)"; [done|].
         iApply ("Post" with "[$P Tkt' NSW]").
         iExists γ, i, n. destruct s. iFrame "Tkt' NSW TCP".
@@ -749,7 +749,7 @@ Section TicketLock.
                                (P ∗ [XP x in (S t) | NSP P γ]_W)%I
                      with "[$P $NSW]"
                   ) as "CEi".
-        iMod (fupd_mask_mono (PROP:=vProp _) with "CEi") as "#CEi"; [namespaces.solve_ndisj|].
+        iMod (fupd_mask_mono with "CEi") as "#CEi"; [namespaces.solve_ndisj|].
         iModIntro. iNext.
         rewrite (unf_int (NSP P γ)).
         iSplitL "".
diff --git a/theories/gps/fractional.v b/theories/gps/fractional.v
index 4c43e02094606381062b671c381015e38c52d828..ff160d850b357490646e6bb8720b5cd3c48e8b6c 100644
--- a/theories/gps/fractional.v
+++ b/theories/gps/fractional.v
@@ -162,9 +162,9 @@ Section Fractional.
           iExists Vr, v. rewrite monPred_in_eq /=.
           iSplit; last iFrame "oR'"; iPureIntro; auto.
           do 4 (etrans; eauto). }
-      iMod ("VS" $! _ j0 with "[% ] [-]") as "VS"; [|by iFrame|].
+      iMod ("VS" $! _ j0 with "[% ] [$]") as "$".
       { repeat (etrans; eauto). }
-      iApply fupd_intro_mask; [solve_ndisj | done]. }
+      iApply fupd_intro_mask'. solve_ndisj. }
     iNext.
     iIntros (s' v Vr V') "(% & kS' & #Hs' & oQ & #oR' & % & %)".
     iFrame.
@@ -230,8 +230,8 @@ Section Fractional.
         + iNext. iExists γ, γ_x, ζ. iFrame; auto.
         + iExists γ, γ_x, e_x. iFrame "Hex". iSplitL ""; first auto.
           iExists V_r, v_r. rewrite monPred_in_eq /=; auto. }
-      iMod ("VS" $! _ j0 with "[//] [$]") as "VS".
-      iApply fupd_intro_mask; [solve_ndisj | done]. }
+      iMod ("VS" $! _ j0 with "[//] [$]") as "$".
+      iApply fupd_intro_mask'. solve_ndisj. }
     iNext.
     iIntros (s' v Vr V'') "(% & kS' & #Hs' & oQ & #oR' & % & %)".
     iFrame.
@@ -413,8 +413,8 @@ Section Fractional.
             iExists Vr, v_n. rewrite monPred_in_eq /=.
             iSplit; last iFrame "oR'"; iPureIntro; auto.
             do 4 (etrans; eauto). }
-        iMod ("Q" $! j0 with "[//] [$oW]").
-        iApply fupd_intro_mask; [solve_ndisj | done].
+        iMod ("Q" $! j0 with "[//] [$oW]") as "$".
+        iApply fupd_intro_mask'. solve_ndisj.
       - by iSpecialize ("VSDup" $! _).
       - iIntros (s' v Vr j ?) "(Hs' & Hv & Fp & (oP & HClose) & % & % & oI & ex & Writer & oR')".
         iDestruct "Writer" as (ζ') "Writer".
@@ -425,9 +425,9 @@ Section Fractional.
             iExists Vr, v. rewrite monPred_in_eq /=.
             iSplit; last iFrame "oR'"; iPureIntro; auto.
             do 4 (etrans; eauto). }
-        iMod ("VSF" $! _ _ _ with "[%] [$Hs' $Hv $Fp $oW $oP]").
+        iMod ("VSF" $! _ _ _ with "[%] [$Hs' $Hv $Fp $oW $oP]") as "$".
         { etrans; eauto. }
-        iApply fupd_intro_mask; [solve_ndisj | done]. }
+        iApply fupd_intro_mask'. solve_ndisj. }
 
     iNext.
     iIntros (s'' b v Vr V')
@@ -463,7 +463,7 @@ Section Fractional.
         iExists s''; iFrame.
         iModIntro; auto.
       - iIntros (??) "(? & ? & ? & ? & ?)"; iFrame.
-        iApply (fupd_mask_mono (PROP:=vProp _)); last by iApply "VSF"; iFrame.
+        iApply fupd_mask_mono; last by iApply "VSF"; iFrame.
         solve_ndisj. }
     iIntros (s'' b v) "(? & ?)".
     destruct b; iApply ("Post" $! s'' _ v); iFrame.
diff --git a/theories/gps/plain.v b/theories/gps/plain.v
index d221c45425d5947b1d3461602e505464ec13559b..5fabc4652a71d9e40f86796ba6f5b2c47a28a54d 100644
--- a/theories/gps/plain.v
+++ b/theories/gps/plain.v
@@ -174,8 +174,8 @@ Section Plain.
           iExists Vr, v.
           iSplit; last iFrame "oR'"; iPureIntro; auto.
           do 4 (etrans; eauto). }
-      iMod ("VS" $! _ j0 with "[%] [-]") as "VS"; [solve_jsl|by iFrame|].
-      iApply fupd_intro_mask; [solve_ndisj | done]. }
+      iMod ("VS" $! _ j0 with "[%] [$]") as "$"; [solve_jsl|].
+      iApply fupd_intro_mask'. solve_ndisj. }
     iNext.
     iIntros (s' v Vr V') "(% & kS' & % & oQ & #oR' & % & %)".
     iFrame. iApply ("Post" $! s' _ _ with "[//]").  by iFrame "%".
@@ -305,8 +305,8 @@ Section Plain.
             iExists Vr, v_n.
             iSplit; last iFrame "oR'"; iPureIntro; auto.
             do 4 (etrans; eauto). }
-        iMod ("Q" $! _ with "[//] [oW //]").
-        iApply fupd_intro_mask; [solve_ndisj | done].
+        iMod ("Q" $! _ with "[//] [oW //]") as "$".
+        iApply fupd_intro_mask'. solve_ndisj.
       - by iSpecialize ("VSDup" $! _).
       - iIntros (s' v Vr j ?) "(Hs' & Hv & Fp & (oP & HClose) & % & % & oI & ex & Writer & oR')".
         iDestruct "Writer" as (ζ') "Writer".
@@ -317,9 +317,9 @@ Section Plain.
             iExists Vr, v.
             iSplit; last iFrame "oR'"; iPureIntro; auto.
             do 4 (etrans; eauto). }
-        iMod ("VSF" $! _ _ _ with "[%] [$Hs' $Hv $Fp $oW $oP]").
+        iMod ("VSF" $! _ _ _ with "[%] [$Hs' $Hv $Fp $oW $oP]") as "$".
         { etrans; eauto. }
-        iApply fupd_intro_mask; [solve_ndisj | done]. }
+        iApply fupd_intro_mask'. solve_ndisj. }
 
     iNext.
     iIntros (s'' b v Vr V')
@@ -354,7 +354,7 @@ Section Plain.
         iExists s''; iFrame.
         iModIntro; auto.
       - iIntros (??) "(? & ? & ? & ? & ?)"; iFrame.
-        iApply (fupd_mask_mono (PROP:=vProp _)); last by iApply "VSF"; iFrame.
+        iApply fupd_mask_mono; last by iApply "VSF"; iFrame.
         solve_ndisj. }
     iIntros (s'' b v) "(? & ?)".
     destruct b; iApply ("Post" $! s'' _ v); iFrame.
diff --git a/theories/gps/singlewriter.v b/theories/gps/singlewriter.v
index 89ab52e8733ddae108590949acd21b83fb08b130..3ba264c4f7cc4b3bcd5e01f757d5826b3012c775 100644
--- a/theories/gps/singlewriter.v
+++ b/theories/gps/singlewriter.v
@@ -411,8 +411,8 @@ Section Gname_StrongSW.
       { iSplit.
         + iNext. iExists γ_x. by iFrame "oI".
         + iExists γ_x. iSplit; first done. iExists Vr, v. by iFrame "oR'". }
-      iMod ("VS" $! _ _ with "[%] [-]") as "VS"; first done; first iFrame.
-      iApply fupd_intro_mask; [solve_ndisj | done]. }
+      iMod ("VS" $! _ _ with "[%] [$]") as "$"; first done.
+      iApply fupd_intro_mask'. solve_ndisj. }
     iNext.
     iIntros (s' v Vr V') "(% & kS' & Hs' & oQ & oR' & % & %)".
     iFrame; iApply ("Post" $! _ _ _ with "[%]"); first done.
@@ -480,9 +480,9 @@ Section Gname_StrongSW.
           { iSplitL "oI".
             + iNext. iExists γ_x. iFrame; auto.
             + iExists γ_x. iSplit; first done. iExists V1, v1. by iFrame "oR1". }
-          iMod ("VS" $! _ _ with "[%] [-]") as "VS"; first done.
+          iMod ("VS" $! _ _ with "[%] [-]") as "$"; first done.
           { iFrame. }
-          iApply fupd_intro_mask; [solve_ndisj | done].
+          iApply fupd_intro_mask'. solve_ndisj.
         - iIntros (s' v ??) "[% Fp]".
           iApply ("VSDup" $! _ s' v _ with "[%] [$Fp]"); first reflexivity.
           iPureIntro. split; [by etrans|auto]. }
@@ -501,9 +501,9 @@ Section Gname_StrongSW.
           { iSplitL "oI".
             + iNext. iExists γ_x. iFrame; auto.
             + iExists γ_x. iSplit; first done. iExists V1, v1. by iFrame "oR1". }
-          iMod ("VS" $! _ _ with "[%] [-]") as "VS"; first done.
+          iMod ("VS" $! _ _ with "[%] [-]") as "$"; first done.
           { iFrame. }
-          iApply fupd_intro_mask; [solve_ndisj | done].
+          iApply fupd_intro_mask'. solve_ndisj.
         - iIntros (s' v ??) "[% Fp]".
           iApply ("VSDup" $! _ s' v _ with "[%] [$Fp]"); first reflexivity.
           iPureIntro. split; solve_jsl. }
@@ -572,9 +572,9 @@ Section Gname_StrongSW.
       { iSplitL "oI".
         + iNext. iExists γ_x. iFrame; auto.
         + iExists γ_x. iSplit; first done. iExists V1, v1. by iFrame "oR". }
-      iMod ("VS" $! _ _ with "[%] [-]") as "VS"; first done.
+      iMod ("VS" $! _ _ with "[%] [-]") as "$"; first done.
       { iFrame. }
-      iApply fupd_intro_mask; [solve_ndisj | done]. }
+      iApply fupd_intro_mask'. solve_ndisj. }
       iNext. iIntros (s' v Vr V'') "(% & kS & % & Q & oR' & % & %)".
       iFrame; iApply ("Post" $! _ _ V'' with "[%]"). { solve_jsl. }
       iMod "Q"; iFrame; auto.
@@ -829,8 +829,8 @@ Section Gname_StrongSW_Param.
       { iSplit.
         + iNext. iExists γ_x. by iFrame "oI".
         + iExists γ_x. iSplit; first done. iExists Vr, v. by iFrame "oR'". }
-      iMod ("VS" $! _ _ with "[%] [-]") as "VS"; first done; first iFrame.
-      iApply fupd_intro_mask; [solve_ndisj | done]. }
+      iMod ("VS" $! _ _ with "[% //] [$]") as "$".
+      iApply fupd_intro_mask'. solve_ndisj. }
     iNext.
     iIntros (s' v Vr V') "(% & kS' & Hs' & >oQ & oR' & % & %)".
     iFrame; iApply ("Post" $! _ _ _ with "[%]"); [solve_jsl|auto].
@@ -1191,8 +1191,8 @@ Section SingleWriter.
       { iSplit.
         + iNext. iExists γ, γ_x. by iFrame "oI".
         + iExists γ, γ_x. iSplit; first done. iExists Vr, v. by iFrame "oR'". }
-      iMod ("VS" $! _ _ with "[%] [-]") as "VS"; first done; first iFrame.
-      iApply fupd_intro_mask; [solve_ndisj | done]. }
+      iMod ("VS" $! _ _ with "[% //] [$]") as "$".
+      iApply fupd_intro_mask'. solve_ndisj. }
     iNext.
     iIntros (s' v Vr V') "(% & kS' & Hs' & oQ & oR' & % & %)".
     iFrame; iApply ("Post" $! _ _ _ with "[%]").
@@ -1373,8 +1373,8 @@ Section SingleWriter.
       { iSplit.
         + iNext. iExists γ, γ_x. by iFrame "oI".
         + iExists γ, γ_x. iSplit; first done. iExists Vr, v. by iFrame "oR'". }
-      iMod ("VS" $! _ _ with "[%] [-]") as "VS"; first done; first iFrame.
-      iApply fupd_intro_mask; [solve_ndisj | done]. }
+      iMod ("VS" $! _ _ with "[% //] [$]") as "$".
+      iApply fupd_intro_mask'. solve_ndisj. }
     iNext.
     iIntros (s' v Vr V') "(% & kS' & Hs' & oQ & oR' & % & %)".
     iFrame; iApply ("Post" $! _ _ _ with "[%]").
diff --git a/theories/weakestpre.v b/theories/weakestpre.v
index d100fd263583172d8015d69a49d77a1247bc671a..6d3e29cb37f9b7074dc2b70a42b36a112a7f1502 100644
--- a/theories/weakestpre.v
+++ b/theories/weakestpre.v
@@ -22,7 +22,6 @@ Import WP_Def.
 Arguments wp {_ _} _ _%E _.
 Instance: Params (@wp) 4.
 
-
 Notation "'WP' e @ E {{ Φ } }" := (wp E e%E Φ)
   (at level 20, e, Φ at level 200,
    format "'WP'  e  @  E  {{  Φ  } }") : bi_scope.
@@ -367,65 +366,18 @@ Section proofmode_classes.
   Proof. by rewrite /IsExcept0 -{2}fupd_wp -except_0_fupd -fupd_intro. Qed.
 
   Global Instance elim_modal_bupd_wp E e P Φ :
-    ElimModal (|==> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
+    ElimModal True (|==> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
   Proof. by rewrite /ElimModal (bupd_fupd E) fupd_frame_r bi.wand_elim_r fupd_wp. Qed.
 
   Global Instance elim_modal_fupd_wp E e P Φ :
-    ElimModal (|={E}=> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
+    ElimModal True (|={E}=> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
   Proof. by rewrite /ElimModal fupd_frame_r bi.wand_elim_r fupd_wp. Qed.
 
   (* lower precedence, if possible, it should always pick elim_upd_fupd_wp *)
   Global Instance elim_modal_fupd_wp_atomic E1 E2 e P Φ :
     (∀ V, Atomic WeaklyAtomic ((e,V) : ra_lang.expr)) →
-    ElimModal (|={E1,E2}=> P) P
+    ElimModal True (|={E1,E2}=> P) P
             (WP e @ E1 {{ Φ }}) (WP e @ E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
   Proof. intros. by rewrite /ElimModal fupd_frame_r bi.wand_elim_r wp_atomic. Qed.
 
 End proofmode_classes.
-
-Section proofmode_classes_embedding.
-  Context `{foundationG Σ}.
-  Implicit Types P Q : vProp Σ.
-  Implicit Types Φ : base.val → vProp Σ.
-
-  Global Instance elim_modal_bupd_wp_emb E e A Φ :
-    ElimModal (⎡|==> A⎤) ⎡A⎤ (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
-  Proof.
-    rewrite /ElimModal.
-    iStartProof (upred.uPredSI _); iIntros (?) "[U WP]".
-    iIntros (V -> π) "kS".
-    iMod "U".
-    iSpecialize ("WP" with "[U //]").
-    iApply ("WP" with "kS").
-  Qed.
-
-  Global Instance elim_modal_fupd_wp_emb E e A Φ :
-    ElimModal (⎡|={E}=> A⎤) ⎡A⎤ (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
-  Proof.
-    rewrite /ElimModal.
-    iStartProof (upred.uPredSI _); iIntros (?) "[U WP]".
-    iIntros (V -> π) "kS".
-    iMod "U".
-    iSpecialize ("WP" with "[U //]").
-    iApply ("WP" with "kS").
-  Qed.
-
-  (* lower precedence, if possible, it should always pick elim_upd_fupd_wp *)
-  Global Instance elim_modal_fupd_wp_atomic_emb E1 E2 e A Φ :
-    (∀ V, Atomic WeaklyAtomic ((e,V) : ra_lang.expr)) →
-    ElimModal (⎡|={E1,E2}=> A⎤) ⎡A⎤
-              (WP e @ E1 {{ Φ }}) (WP e @ E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
-  Proof.
-    rewrite /ElimModal.
-    iStartProof (upred.uPredSI _). iIntros (??) "[U WP]".
-    iIntros (V -> π) "kS".
-    iMod "U".
-    iSpecialize ("WP" with "[U //]").
-    iApply iris.program_logic.weakestpre.wp_mono; cycle 1.
-    iApply ("WP" with "kS").
-    by iIntros ([v V']) "[$ >$]".
-  Qed.
-
-End proofmode_classes_embedding.
-
-Delimit Scope val_scope with Val. (* TODO: what is this? *)
diff --git a/theories/wp_tactics.v b/theories/wp_tactics.v
index 8c7462f391f4e807ecb413ce509ab4991ac743f4..6f00bcf0e8683745f8accd40b7037123a7dc2f8b 100644
--- a/theories/wp_tactics.v
+++ b/theories/wp_tactics.v
@@ -12,7 +12,7 @@ Lemma tac_wp_pure `{ghosts.foundationG Σ} K Δ Δ' E e1 e2 φ Φ :
   envs_entails Δ' (WP fill K e2 @ E {{ Φ }}) →
   envs_entails Δ (WP fill K e1 @ E {{ Φ }}).
 Proof.
-  rewrite /envs_entails=> ??? HΔ'. rewrite into_laterN_env_sound /=.
+  rewrite envs_entails_eq=> ??? HΔ'. rewrite into_laterN_env_sound /=.
   rewrite -weakestpre.wp_bind HΔ' -lifting.wp_pure_step_later //.
   by rewrite -weakestpre.wp_bind_inv.
 Qed.
@@ -20,7 +20,7 @@ Qed.
 Lemma tac_wp_value `{ghosts.foundationG Σ} Δ E Φ e v :
   IntoVal e v →
   envs_entails Δ (Φ v) → envs_entails Δ (WP e @ E {{ Φ }}).
-Proof. rewrite /envs_entails=> ? ->. by apply wp_value. Qed.
+Proof. rewrite envs_entails_eq=> ? ->. by apply wp_value. Qed.
 
 Ltac wp_value_head := eapply tac_wp_value; [apply _|lazy beta].
 
@@ -53,7 +53,7 @@ Tactic Notation "wp_seq" := wp_lam.
 Lemma tac_wp_bind `{ghosts.foundationG Σ} K Δ E Φ e :
   envs_entails Δ (WP e @ E {{ v, WP fill K (ectxi_language.of_val v) @ E {{ Φ }} }})%I →
   envs_entails Δ (WP fill K e @ E {{ Φ }}).
-Proof. rewrite /envs_entails=> ->. exact: wp_bind. Qed.
+Proof. rewrite envs_entails_eq=> ->. exact: wp_bind. Qed.
 
 Ltac wp_bind_core K :=
   lazymatch eval hnf in K with
diff --git a/theories/wp_tactics_vProp.v b/theories/wp_tactics_vProp.v
index 1f64da172620c9f356f90112bd699008642d4529..9d2c54176c798e55dd5f6e7b913e66f521773c3a 100644
--- a/theories/wp_tactics_vProp.v
+++ b/theories/wp_tactics_vProp.v
@@ -23,14 +23,14 @@ Lemma tac_wp_pure `{foundationG Σ} Δ Δ' E e1 e2 φ Φ :
   envs_entails Δ' (WP e2 @ E {{ Φ }}) →
   envs_entails Δ (WP e1 @ E {{ Φ }}).
 Proof.
-  rewrite /envs_entails=> ??? HΔ'. rewrite into_laterN_env_sound /=.
+  rewrite envs_entails_eq=> ??? HΔ'. rewrite into_laterN_env_sound /=.
   rewrite HΔ' -wp_pure_step_later //.
 Qed.
 
 Lemma tac_wp_value `{foundationG Σ} Δ E Φ e v :
   (IntoVal (e) (v)) →
   envs_entails Δ (Φ v) → envs_entails Δ (WP e @ E {{ Φ }}).
-Proof. rewrite /envs_entails=> IV ->. now apply: wp_value. Qed.
+Proof. rewrite envs_entails_eq=> IV ->. now apply: wp_value. Qed.
 
 Ltac wp_value_head := eapply tac_wp_value; [apply _|lazy beta].
 
@@ -67,7 +67,7 @@ Tactic Notation "wp_seq" := wp_lam.
 Lemma tac_wp_bind `{foundationG Σ} K Δ E Φ e :
   envs_entails Δ (WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }})%I →
   envs_entails Δ (WP fill K e @ E {{ Φ }}).
-Proof. rewrite /envs_entails=> ->. by apply wp_bind. Qed.
+Proof. rewrite envs_entails_eq=> ->. by apply wp_bind. Qed.
 
 Ltac wp_bind_core K :=
   lazymatch eval hnf in K with