diff --git a/opam b/opam
index 4ffe52fc3bbf9abc82bd73449b72a585a0238929..78b4fe3c88f76868791094fafb94e36f568dd710 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-19.0") | (= "dev") }
+  "coq-iris" { (= "branch.gen_proofmode.2018-03-21.0") | (= "dev") }
 ]
diff --git a/theories/examples/circ_buffer.v b/theories/examples/circ_buffer.v
index a6381fd865e565666dd73652d0c24e8c13148be3..196499864ed5e68a208481584b4af85a9f710e8e 100644
--- a/theories/examples/circ_buffer.v
+++ b/theories/examples/circ_buffer.v
@@ -286,19 +286,18 @@ Section CircBuffer.
       wp_lam. wp_bind ([_]_at)%E. wp_op.
 
       iApply (GPS_SW_Read_ex with "[$kI $pW]"); [done|done|..].
-      { rewrite monPred_objectively_unfold. iIntros (????) "!> #$ //". }
+      { by iIntros "/= !> !> % #$ !>". }
 
       iNext. iIntros (w) "(pW & #CEs)".
       iDestruct "CEs" as "(% & CEs)".
 
-
       wp_let. wp_bind ([_]_at)%E. wp_op.
 
       iApply (GPS_SW_Read (consInt γ q) True%I (CP (γ,q))
                 with "[$kI $cR]"); [done|done|..].
       { iSplitL.
-        - iIntros (?). iIntros "_". iLeft. by iIntros "!>" (?) "(? & _)".
-        - rewrite monPred_objectively_unfold. iIntros "!>" (?????) "[? #$] //". }
+        - iIntros (?) "_". iLeft. by iIntros "!>" (?) "(? & _)".
+        - by iIntros "/= !> !> %% [_ #$] !>". }
 
       iNext. iIntros (j r) "(% & #cR2 & #PEs)".
       iDestruct "PEs" as "(% & PEs)".
@@ -390,7 +389,7 @@ Section CircBuffer.
                 with "[$kI $pR]"); [done|done|..].
       { iSplitL.
         - iIntros (??). iLeft. iIntros "!>" (?) "(? & _)". by auto.
-        - rewrite monPred_objectively_unfold. iIntros "!>" (?????) "[? #$] //". }
+        - by iIntros "!> !> %% [_ #$] !>". }
 
       iNext. iIntros (i w) "(% & pR & #CEs)".
       iDestruct "CEs" as "(% & CEs)".
@@ -399,7 +398,7 @@ Section CircBuffer.
 
       iApply (GPS_SW_Read_ex
                 with "[$kI $cW]"); [done|done|..].
-      { rewrite monPred_objectively_unfold. iIntros "!>" (????) "!> #$ //". }
+      { by iIntros "!> !> % #$ !>". }
 
       iNext. iIntros (r) "(cW & #PEs)".
       iDestruct "PEs" as "(% & PEs)".
diff --git a/theories/gps/singlewriter.v b/theories/gps/singlewriter.v
index 24de2fe241fa53c71c026b6f50c004219344779e..fde8c74be08951babd18254e675dbfc5cc8ed8d5 100644
--- a/theories/gps/singlewriter.v
+++ b/theories/gps/singlewriter.v
@@ -1021,7 +1021,7 @@ Section SingleWriter.
   Local Instance :
     Frame false (gps_inv IP l γ γ_x) (gpsSWRaw l (encode (γ, (γ_x)))) True.
   Proof.
-    intros. unfold Frame, bi_affinely_if, bi_persistently_if.
+    intros. unfold Frame, bi_intuitionistically_if.
     iIntros "[H _]". iExists _, _. by iFrame "∗".
   Qed.
   Local Close Scope I.
@@ -1752,4 +1752,4 @@ Global Instance vGPS_nWSP_proper `{persistorG Σ, EqDecision Param, Countable Pa
 Proof.
   split=>?. rewrite !vGPS_nWSP_eq /=. subst. f_equiv=>??. by apply gpsSWpnRaw_proper.
 Qed.
-End proper.
\ No newline at end of file
+End proper.
diff --git a/theories/rsl.v b/theories/rsl.v
index dfab4f3ac266f7e7cfaf2dd688d7999669d244d0..b0c375eb569666b122edad6b47bd04f1c77227c5 100644
--- a/theories/rsl.v
+++ b/theories/rsl.v
@@ -172,7 +172,7 @@ Instance InitRaw_persistent V jγ : Persistent (InitRaw V jγ) := _.
     iExists (<[i:= (λ _ _, True)]> Ψ). iSplitL "Saved".
     - rewrite (big_sepS_fn_insert (λ i0 f, saved_anything_own i0 (to_saved f)));
        last exact NI. by iFrame.
-    - iNext. rewrite affinely_persistently_elim. iIntros "!#".
+    - iNext. rewrite intuitionistically_elim. iIntros "!#".
       iIntros (i' v' V') "In".
       iDestruct "In" as %[->%elem_of_singleton_1|In]%elem_of_union.
       + rewrite fn_lookup_insert. iSplit; by iIntros "_".