diff --git a/opam b/opam
index 7af1e70aef7c3303221e07053293e1c117815e5c..99972c63a69ca93c4748be863fa574ced2608a56 100644
--- a/opam
+++ b/opam
@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/reloc"]
 depends: [
-  "coq-iris" { (= "dev.2020-04-02.5.fa438702") | (= "dev") }
+  "coq-iris" { (= "dev.2020-04-04.3.9b2ad256") | (= "dev") }
   "coq-autosubst" { = "dev.coq86" }
 ]
diff --git a/theories/experimental/helping/helping_stack.v b/theories/experimental/helping/helping_stack.v
index cb1877a4282fd649f8e74545dc6c3975d3e5969d..8bbf9cb88327adf13cd4d44e5bf30f19ace686c3 100644
--- a/theories/experimental/helping/helping_stack.v
+++ b/theories/experimental/helping/helping_stack.v
@@ -124,7 +124,7 @@ Section refinement.
       rewrite auth_auth_valid. done. }
     iPureIntro.
     revert Hfoo.
-    rewrite singleton_included=> -[av []].
+    rewrite singleton_included_l=> -[av []].
     revert Hvalid.
     rewrite /to_offer_reg !lookup_fmap.
     case: (N !! o)=> [av'|] Hvalid; last by inversion 1.
diff --git a/theories/logic/spec_ra.v b/theories/logic/spec_ra.v
index e5cff14c44acc0839abc7b3744505861f8cb9237..ef586ca870027cbfcdce3e790e7996bf74d14ad8 100644
--- a/theories/logic/spec_ra.v
+++ b/theories/logic/spec_ra.v
@@ -113,7 +113,7 @@ Section conversions.
   Lemma tpool_singleton_included tp j e :
     {[j := Excl e]} ≼ to_tpool tp → tp !! j = Some e.
   Proof.
-    move=> /singleton_included [ex [/leibniz_equiv_iff]].
+    move=> /singleton_included_l [ex [/leibniz_equiv_iff]].
     rewrite tpool_lookup fmap_Some=> [[e' [-> ->]] /Excl_included ?]. by f_equal.
   Qed.
   Lemma tpool_singleton_included' tp j e :