diff --git a/opam b/opam
index f88680d1cb7b4c08185dbd2de22f724a18268232..acb47be8c1a85bfc9109a74007e72fbf59676de3 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-04.7") | (= "dev") }
+  "coq-iris" { (= "branch.gen_proofmode.2018-03-09.0") | (= "dev") }
 ]
diff --git a/theories/examples/message_passing.v b/theories/examples/message_passing.v
index e1a56e42e1afb06aa740edd079f37b77630bc964..ddfddd8b37565f1d247cafae4901b536a642cbaf 100644
--- a/theories/examples/message_passing.v
+++ b/theories/examples/message_passing.v
@@ -104,7 +104,6 @@ Section proof.
           iDestruct (escrow_apply (Tok γ) (x ↦ 37))%I as "EA".
           iSpecialize ("EA" with "[]").
           { iIntros "?". by iApply unit_tok_exclusive. }
-          erewrite bool_decide_false; last auto.
           iSpecialize ("EA" with "[$XE $Tok]").
           iNext. iNext.
           iApply fupd_wp. iMod (fupd_mask_mono with "EA") as "Nax"; [done|].
diff --git a/theories/gps/fractional.v b/theories/gps/fractional.v
index aaee3cc60502ef8e4dae692746f0741fd684f762..541f163af068205705f03e575ed6b909bf61d46e 100644
--- a/theories/gps/fractional.v
+++ b/theories/gps/fractional.v
@@ -152,8 +152,7 @@ Section Fractional.
     { iSplitR "VSDup"; iNext; last by iSpecialize ("VSDup" $! _).
       iIntros (s' j ? Hs').
       iDestruct ("VS" $! _ Hs') as "[VS|VS]"; last first.
-      { iRight. iIntros (?????). iApply ("VS" $! _ _ _ with "[%] [%//]").
-        repeat etrans=>//. }
+      { iRight. iIntros (?????). by iApply ("VS" $! _ _ with "[%]"). }
       iLeft; iIntros (v Vr j0 Hle') "(? & ? & % & % & oI & oR')".
       iMod ("HClose" $! (RFRaw s' j0) with "[Writer oI oR' Hex]").
       { iSplitL "oI Writer".
@@ -223,14 +222,14 @@ Section Fractional.
       [solve_ndisj|solve_jsl|..].
     { iSplitR "VSDup"; last by iSpecialize ("VSDup" $! _).
       iIntros (s' j ? Hs').
-      iDestruct ("VS" $! _ j with "[%] [%//]") as "[VS|VS]"; [solve_jsl| |by iRight].
+      iDestruct ("VS" $! _ with "[%//]") as "[VS|VS]"; last by auto.
       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.
         + iExists γ, γ_x, e_x. iFrame "Hex". iSplitL ""; first auto.
           iExists V_r, v_r. rewrite monPred_in_eq /=; auto. }
-      iMod ("VS" $! _ j0 with "[//] [$]") as "$".
+      iMod ("VS" $! _ j0 with "[%] [$]") as "$"; [solve_jsl|].
       iApply fupd_intro_mask'. solve_ndisj. }
     iNext.
     iIntros (s' v Vr V'') "(% & kS' & #Hs' & oQ & #oR' & % & %)".
diff --git a/theories/gps/plain.v b/theories/gps/plain.v
index 6f5a405cb6675731068e8da0f8402891ccf06606..57997687031a5eb32636d845654ce2bd8e9f778b 100644
--- a/theories/gps/plain.v
+++ b/theories/gps/plain.v
@@ -165,21 +165,19 @@ Section Plain.
     { etransitivity; eauto. }
     { iSplitR "VSDup"; iNext; last by iSpecialize ("VSDup" $! _).
       iIntros (s' j ? Hs'). iDestruct ("VS" $! s' Hs') as "[VS|VS]"; last first.
-      { iRight. iIntros (?????). iApply ("VS" $! _ _ _ with "[%] [//]").
-        repeat etrans=>//. }
+      { iRight. iIntros (?????). iApply ("VS" $! _ _ with "[//]"). }
       iLeft; iIntros (v Vr j0 Hle') "(? & ? & % & % & oI & oR')".
       iMod ("HClose" $! (RPRaw p s' j0) with "[Writer oI oR' Ex]").
       { iSplit.
         + iNext. iExists γ, γ_x, γx, e_x, ζ. iFrame; auto.
         + iExists γ, γ_x, γx, e_x. iFrame "Hex". iSplitL ""; first auto.
-          iExists Vr, v.
-          iSplit; last iFrame "oR'"; iPureIntro; auto.
+          iExists Vr, v. iSplit; last iFrame "oR'"; iPureIntro; auto.
           do 4 (etrans; eauto). }
       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 "%".
+    iFrame. iApply ("Post" $! s' _ _ with "[//]"). by iFrame "%".
   Qed.
 
   Lemma GPS_PP_Read l p (P : vPred) (Q : pr_state Prtcl → Z → vPred)
diff --git a/theories/gps/read.v b/theories/gps/read.v
index b59f18d8d220f7765391e79a8c3b6b1ef4bcaa8d..4afbe26849ee4e55c0d532b72303f73b6ac2288b 100644
--- a/theories/gps/read.v
+++ b/theories/gps/read.v
@@ -104,13 +104,12 @@ Section Read.
               eapply (Pos.lt_le_trans); last exact Le.
               by apply Pos.lt_add_r. }
 
-        iAssert (⌜s' ⊑ st_prst e⌝)%I as "Hse".
-          { iPureIntro. by apply (H0 _ _ In Ine), He. }
+        assert (Hse : s' ⊑ st_prst e) by by apply (H0 _ _ In Ine), He.
 
         rewrite /BE_Inv (bi.big_sepS_delete _ _ _ Heb).
         iDestruct "oBEI" as "[F oBEI]".
-        iMod ("VS" $! (st_prst e) (st_val e) (V ⊔ (st_view e))
-             with "[%] [$Hse] [$F $P]") as "[]". solve_jsl.
+        iMod ("VS" $! (st_prst e) (st_val e) Hse (V ⊔ (st_view e))
+             with "[%] [$F $P]") as "[]". solve_jsl.
   Qed.
 
 
diff --git a/theories/gps/singlewriter.v b/theories/gps/singlewriter.v
index 27937e56d1b75e92b1447214549444f2098b39f6..24de2fe241fa53c71c026b6f50c004219344779e 100644
--- a/theories/gps/singlewriter.v
+++ b/theories/gps/singlewriter.v
@@ -404,17 +404,16 @@ 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|..].
     { iSplitR "VSDup"; last by iSpecialize ("VSDup" $! _).
-      iIntros "!>" (s' j ?) "Hs'".
-      iDestruct ("VS" $! _ j with "[//] [Hs' //]") as "[VS|VS]"; last by iRight.
+      iIntros "!>" (s' j ? Hs').
+      iDestruct ("VS" $! _ Hs') as "[VS|VS]"; last by auto with iFrame.
       iLeft; iIntros (v Vr j0 Hle') "(? & ? & % & % & oI & oR')".
       iMod ("HClose" $! (fun l _ p => ReaderSWnRaw γ s' j0 l p) with "[oI oR']").
       { iSplit.
         + iNext. iExists γ_x. by iFrame "oI".
         + iExists γ_x. iSplit; first done. iExists Vr, v. by iFrame "oR'". }
-      iMod ("VS" $! _ _ with "[%] [$]") as "$"; first done.
+      iMod ("VS" $! _ _ with "[%] [$]") as "$"; first solve_jsl.
       iApply fupd_intro_mask'. solve_ndisj. }
-    iNext.
-    iIntros (s' v Vr V') "(% & kS' & Hs' & oQ & oR' & % & %)".
+    iIntros "!>" (s' v Vr V') "(% & kS' & Hs' & oQ & oR' & % & %)".
     iFrame; iApply ("Post" $! _ _ _ with "[%]"); first done.
     by iFrame "Hs'".
   Qed.
@@ -473,14 +472,14 @@ Section Gname_StrongSW.
                 with "[$oI $kI $kS $oP $oR2 VS VSDup HClose]"); [solve_ndisj|solve_jsl|..].
       { iSplitR "VSDup".
         - iIntros (s' j ??).
-          iDestruct ("VS" $! _ _ with "[%] [%]") as "[VS|VS]"; last by iRight.
-          { solve_jsl. } { split; solve_jsl. }
+          iDestruct ("VS" $! _ with "[%]") as "[VS|VS]"; last by auto with iFrame.
+          { split; solve_jsl. }
           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.
             + iExists γ_x. iSplit; first done. iExists V1, v1. by iFrame "oR1". }
-          iMod ("VS" $! _ _ with "[%] [-]") as "$"; first done.
+          iMod ("VS" $! _ _ with "[%] [-]") as "$"; first solve_jsl.
           { iFrame. }
           iApply fupd_intro_mask'. solve_ndisj.
         - iIntros "!>" (s' v ??) "[% Fp]".
@@ -494,14 +493,14 @@ Section Gname_StrongSW.
                 with "[$oI $kI $kS $oP $oR1 VS VSDup HClose]"); [solve_ndisj|solve_jsl|..].
       { iSplitR "VSDup".
         - iIntros (s' j ??).
-          iDestruct ("VS" $! _ _ with "[%] [%]") as "[VS|VS]"; last by iRight.
-          { solve_jsl. } { split; solve_jsl. }
+          iDestruct ("VS" $! _ with "[%]") as "[VS|VS]"; last by auto with iFrame.
+          { split; solve_jsl. }
           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.
             + iExists γ_x. iSplit; first done. iExists V1, v1. by iFrame "oR1". }
-          iMod ("VS" $! _ _ with "[%] [-]") as "$"; first done.
+          iMod ("VS" $! _ _ with "[%] [-]") as "$"; first solve_jsl.
           { iFrame. }
           iApply fupd_intro_mask'. solve_ndisj.
         - iIntros "!>" (s' v ??) "[% Fp]".
@@ -565,14 +564,13 @@ Section Gname_StrongSW.
     { solve_jsl. }
     { iSplitR "VSDup"; last by iSpecialize ("VSDup" $! _).
       iIntros (s' j ??).
-      iDestruct ("VS" $! _ _ with "[%] [//]") as "[VS|VS]"; last by iRight.
-      { solve_jsl. }
+      iDestruct ("VS" $! _ with "[% //]") as "[VS|VS]"; last by auto with iFrame.
       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.
         + iExists γ_x. iSplit; first done. iExists V1, v1. by iFrame "oR". }
-      iMod ("VS" $! _ _ with "[%] [-]") as "$"; first done.
+      iMod ("VS" $! _ _ with "[%] [-]") as "$"; first solve_jsl.
       { iFrame. }
       iApply fupd_intro_mask'. solve_ndisj. }
       iNext. iIntros (s' v Vr V'') "(% & kS & % & Q & oR' & % & %)".
@@ -822,14 +820,13 @@ Section Gname_StrongSW_Param.
     { etrans; eauto. }
     { iSplitR "VSDup"; last by iSpecialize ("VSDup" $! _).
       iIntros (s' j ? Hs').
-      iDestruct ("VS" $! _ Hs' j with "[%]") as "[VS|VS]"; last by iRight.
-      { etrans; eauto. }
+      iDestruct ("VS" $! _ Hs') as "[VS|VS]"; last by auto with iFrame.
       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".
         + iExists γ_x. iSplit; first done. iExists Vr, v. by iFrame "oR'". }
-      iMod ("VS" $! _ _ with "[% //] [$]") as "$".
+      iMod ("VS" $! _ _ with "[%] [$]") as "$"; [solve_jsl|].
       iApply fupd_intro_mask'. solve_ndisj. }
     iNext.
     iIntros (s' v Vr V') "(% & kS' & Hs' & >oQ & oR' & % & %)".
@@ -1184,17 +1181,15 @@ Section SingleWriter.
     { etrans; eauto. }
     { iSplitR "VSDup"; last by iSpecialize ("VSDup" $! _).
       iIntros (s' j ? Hs').
-      iDestruct ("VS" $! _ Hs' j with "[%]") as "[VS|VS]"; last by iRight.
-      { etrans; eauto. }
+      iDestruct ("VS" $! _ Hs') as "[VS|VS]"; last by auto with iFrame.
       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".
         + iExists γ, γ_x. iSplit; first done. iExists Vr, v. by iFrame "oR'". }
-      iMod ("VS" $! _ _ with "[% //] [$]") as "$".
+      iMod ("VS" $! _ _ with "[%] [$]") as "$"; [solve_jsl|].
       iApply fupd_intro_mask'. solve_ndisj. }
-    iNext.
-    iIntros (s' v Vr V') "(% & kS' & Hs' & oQ & oR' & % & %)".
+    iIntros "!>" (s' v Vr V') "(% & kS' & Hs' & oQ & oR' & % & %)".
     iFrame; iApply ("Post" $! _ _ _ with "[%]").
     { etrans; eauto. }
     by iFrame "Hs'".
@@ -1366,17 +1361,15 @@ Section SingleWriter.
     { etrans; eauto. }
     { iSplitR "VSDup"; last by iSpecialize ("VSDup" $! _).
       iIntros (s' j ? Hs').
-      iDestruct ("VS" $! _ Hs' j with "[%]") as "[VS|VS]"; last by iRight.
-      { etrans; eauto. }
+      iDestruct ("VS" $! _ Hs') as "[VS|VS]"; last by auto with iFrame.
       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".
         + iExists γ, γ_x. iSplit; first done. iExists Vr, v. by iFrame "oR'". }
-      iMod ("VS" $! _ _ with "[% //] [$]") as "$".
+      iMod ("VS" $! _ _ with "[%] [$]") as "$"; [solve_jsl|].
       iApply fupd_intro_mask'. solve_ndisj. }
-    iNext.
-    iIntros (s' v Vr V') "(% & kS' & Hs' & oQ & oR' & % & %)".
+    iIntros "!>" (s' v Vr V') "(% & kS' & Hs' & oQ & oR' & % & %)".
     iFrame; iApply ("Post" $! _ _ _ with "[%]").
     { etrans; eauto. }
     by iFrame "Hs'".
diff --git a/theories/malloc.v b/theories/malloc.v
index 955e5237b14d8c68ae21fe6a75c5f504c6fb7a2a..c3cd41732a21bef61156c41449e3df1f0c3276ce 100644
--- a/theories/malloc.v
+++ b/theories/malloc.v
@@ -71,8 +71,7 @@ Section proof.
     iDestruct "oL" as (h i) "(Alloc & oH & oI)".
     rewrite HV2. rewrite {1}HV3.
     iApply (f_dealloc with "[$kI $kS $oH $oI $Alloc]").
-    iNext. iIntros (?) "(% & $)".
-    iApply ("Post" $! _ with "[%] [-]"); [etrans;done|done].
+    iNext. iIntros (?) "(% & $)". by iApply "Post".
   Qed.
 
   Lemma mdealloc_spec (l: loc) (n : Z) :
@@ -175,7 +174,7 @@ Section proof.
         wp_op.
 
         iApply ("IHmall" $! (z+1) (n-1) with "[%] [%] [%] [$Post] [Big oL]");
-          [omega|omega|omega|..].
+          [omega..|].
 
         rewrite Z2Nat.inj_succ; last omega.
         rewrite seq_S big_opL_app bi.big_sepL_singleton.
diff --git a/theories/rsl.v b/theories/rsl.v
index 592ad208b15c7a121eca345e3365fb3a0c580fa4..dfab4f3ac266f7e7cfaf2dd688d7999669d244d0 100644
--- a/theories/rsl.v
+++ b/theories/rsl.v
@@ -949,9 +949,8 @@ Instance InitRaw_persistent V jγ : Persistent (InitRaw V jγ) := _.
         * right. by eexists.
         * by exists (VInj v_w), V'.
 
-    - iDestruct "CF" as "(% & #NE & % & %)".
-      iMod ("CFail" $! v V' with "[//] [NE//] [$P $Hφd]") as "R".
-
+    - iDestruct "CF" as %(? & NE & ? & ?).
+      iMod ("CFail" $! v NE V' with "[//] [$P $Hφd]") as "R".
       rewrite -sts_op_auth_frag_up.
       iDestruct "Own" as "(Own & #Own')".
 
diff --git a/theories/tests/message_passing.v b/theories/tests/message_passing.v
index 518033fc27019b0065452ee7dc2210f5978cecaf..cc85428318af9cb033d4a9674b2fb57b33c9787b 100644
--- a/theories/tests/message_passing.v
+++ b/theories/tests/message_passing.v
@@ -30,12 +30,10 @@ Proof.
     { by auto. }
     iModIntro.
     iPoseProof (message_passing_spec (fun v => ⌜v = #37⌝)%I with "[$PS $Pers]") as "T".
-    iSpecialize ("T" $! ∅ with "[%]"); [reflexivity|].
-    rewrite WP_Def.wp_eq /WP_Def.wp_def. cbn.
-    iApply wp_mono; cycle 1.
-    + iApply "T"; [|done|done].
-      iNext. iIntros. iPureIntro. intros []. done.
-    + iIntros ([v ?]) "[_ %]". subst v. done.
+    iSpecialize ("T" with "[%]"); [by intros ? ->|].
+    rewrite WP_Def.wp_eq /WP_Def.wp_def /=. iApply wp_mono; cycle 1.
+    + by iApply "T".
+    + by iIntros ([v ?]) "[_ %]".
 Qed.
 
 Print Assumptions message_passing.