Bump Iris.

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") }
 ]

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:

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 :

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.