diff --git a/opam b/opam
index 89b8bb9ef33189b9e69aab805897148188e9b560..75e892b8da0197a8750cb4c6d82e4e4c8c70939a 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-21.3") | (= "dev") }
+  "coq-iris" { (= "branch.gen_proofmode.2018-04-05.1") | (= "dev") }
 ]
diff --git a/theories/weakestpre.v b/theories/weakestpre.v
index 4af5c4a9420788b08d74fc0ce28270f272800d87..b36a478e59766e1446840e09125f3336980e61ab 100644
--- a/theories/weakestpre.v
+++ b/theories/weakestpre.v
@@ -366,19 +366,28 @@ Section proofmode_classes.
   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.
 
-  Global Instance elim_modal_bupd_wp E e P Φ :
-    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_bupd_wp p E e P Φ :
+    ElimModal True p false (|==> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
+  Proof.
+    by rewrite /ElimModal bi.intuitionistically_if_elim (bupd_fupd E)
+      fupd_frame_r bi.wand_elim_r fupd_wp.
+  Qed.
 
-  Global Instance elim_modal_fupd_wp E e P Φ :
-    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.
+  Global Instance elim_modal_fupd_wp p E e P Φ :
+    ElimModal True p false (|={E}=> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
+  Proof.
+    by rewrite /ElimModal bi.intuitionistically_if_elim
+      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 Φ :
+  Global Instance elim_modal_fupd_wp_atomic p E1 E2 e P Φ :
     (∀ V, Atomic WeaklyAtomic ((e,V) : ra_lang.expr)) →
-    ElimModal True (|={E1,E2}=> P) P
+    ElimModal True p false (|={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.
+  Proof.
+    intros. by rewrite /ElimModal bi.intuitionistically_if_elim
+      fupd_frame_r bi.wand_elim_r wp_atomic.
+  Qed.
 
 End proofmode_classes.