diff --git a/opam b/opam
index 6e9e09bbceb534500faab2a5665ac50c5cafc4cc..a33985ab43108f95984a4c4cd1b478abac9f6db7 100644
--- a/opam
+++ b/opam
@@ -11,5 +11,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
 depends: [
-  "coq-iris" { (= "dev.2019-04-25.1.a9031f7f") | (= "dev") }
+  "coq-iris" { (= "dev.2019-05-01.1.c7164230") | (= "dev") }
 ]
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index 38b1406200ed9089d7b1cd97e742a9b70a94d31b..2c3acda7993eef04768f3705dfa9c426fd164a53 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -129,7 +129,7 @@ Section heap.
 
   Global Instance heap_mapsto_vec_fractional l vl: Fractional (λ q, l ↦∗{q} vl)%I.
   Proof.
-    intros p q. rewrite /heap_mapsto_vec -big_sepL_sepL.
+    intros p q. rewrite /heap_mapsto_vec -big_sepL_sep.
     by setoid_rewrite (fractional (Φ := λ q, _ ↦{q} _)%I).
   Qed.
   Global Instance heap_mapsto_vec_as_fractional l q vl:
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index c633f1dd66ab73ef976220e7bbce4ea4c48b107c..4086a8242518b082a6fe2a6fb9f3d4cb006b1f62 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -289,7 +289,7 @@ Proof. rewrite /lft_dead. iDestruct 1 as (Λ) "[% H']". set_solver. Qed.
 (* Fractional and AsFractional instances *)
 Global Instance lft_tok_fractional κ : Fractional (λ q, q.[κ])%I.
 Proof.
-  intros p q. rewrite /lft_tok -big_sepMS_sepMS. apply big_sepMS_proper.
+  intros p q. rewrite /lft_tok -big_sepMS_sep. apply big_sepMS_proper.
   intros Λ ?. rewrite -Cinl_op -op_singleton auth_frag_op own_op //.
 Qed.
 Global Instance lft_tok_as_fractional κ q :
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index eead3bd411a37cf215e727badb32e041804fb718..89829f2ef02d3b306a12ec078eac671f272a38fd 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -60,7 +60,7 @@ Section lft_contexts.
   Global Arguments llctx_interp _ _%Qp.
   Global Instance llctx_interp_fractional L :
     Fractional (llctx_interp L).
-  Proof. intros ??. rewrite -big_sepL_sepL. by setoid_rewrite <-fractional. Qed.
+  Proof. intros ??. rewrite -big_sepL_sep. by setoid_rewrite <-fractional. Qed.
   Global Instance llctx_interp_as_fractional L q :
     AsFractional (llctx_interp L q) (llctx_interp L) q.
   Proof. split. done. apply _. Qed.