diff --git a/opam b/opam
index 272902f373af97bdcf7a7150ba893433904709f6..0ffbd247423bf66d992ecf11d4e526f7f4753d2d 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-09-19.0.ca3f9d11") | (= "dev") }
+  "coq-iris" { (= "dev.2019-09-19.3.aa7871c7") | (= "dev") }
 ]
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index d7ec26143e37de25724431cb0d7b1f3e76de009c..4abef3c1c3b1c079964dd2f5428eb0e3c7309f85 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -174,7 +174,7 @@ Section heap.
       { rewrite !heap_mapsto_vec_nil. iIntros "_"; auto. }
       rewrite !heap_mapsto_vec_cons. iIntros "[[Hv1 Hvl1] [Hv2 Hvl2]]".
       iDestruct (IH (l +ₗ 1) with "[$Hvl1 $Hvl2]") as "[% $]"; subst.
-      rewrite (inj_iff (:: vl2)).
+      rewrite (inj_iff (.:: vl2)).
       iDestruct (heap_mapsto_agree with "[$Hv1 $Hv2]") as %<-.
       iSplit; first done. iFrame.
     - by iIntros "[% [$ Hl2]]"; subst.
diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index 6ce23b84649824ac722949ec7300794ae5454046..06af6e4e67fa7e33d049c60ee9caa742dd811201 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -430,13 +430,13 @@ Qed.
 
 Definition fresh_block (σ : state) : block :=
   let loclst : list loc := elements (dom _ σ : gset loc) in
-  let blockset : gset block := foldr (λ l, ({[l.1]} ∪)) ∅ loclst in
+  let blockset : gset block := foldr (λ l, ({[l.1]} ∪.)) ∅ loclst in
   fresh blockset.
 
 Lemma is_fresh_block σ i : σ !! (fresh_block σ,i) = None.
 Proof.
   assert (∀ (l : loc) ls (X : gset block),
-    l ∈ ls → l.1 ∈ foldr (λ l, ({[l.1]} ∪)) X ls) as help.
+    l ∈ ls → l.1 ∈ foldr (λ l, ({[l.1]} ∪.)) X ls) as help.
   { induction 1; set_solver. }
   rewrite /fresh_block /shift_loc /= -(not_elem_of_dom (D := gset loc)) -elem_of_elements.
   move=> /(help _ _ ∅) /=. apply is_fresh.
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 773117282efae71db82f51d5e40307d970a41a5e..10a2939877119948003922343606d5fd397a578c 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -54,8 +54,8 @@ Module Type lifetime_sig.
 
   Global Declare Instance lft_intersect_comm : Comm (A:=lft) eq (⊓).
   Global Declare Instance lft_intersect_assoc : Assoc (A:=lft) eq (⊓).
-  Global Declare Instance lft_intersect_inj_1 (κ : lft) : Inj eq eq (κ ⊓).
-  Global Declare Instance lft_intersect_inj_2 (κ : lft) : Inj eq eq (⊓ κ).
+  Global Declare Instance lft_intersect_inj_1 (κ : lft) : Inj eq eq (κ ⊓.).
+  Global Declare Instance lft_intersect_inj_2 (κ : lft) : Inj eq eq (.⊓ κ).
   Global Declare Instance lft_intersect_left_id : LeftId eq static meet.
   Global Declare Instance lft_intersect_right_id : RightId eq static meet.
 
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index 72ed90493ad28c5bf259811b68e8b3cfdbf9d4db..e0862b40427ee838eccd6bd67245cfc9d35eceb9 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -36,14 +36,14 @@ Proof.
   iMod (box_empty with "Hbox") as "[HP Hbox]"=>//; first set_solver.
   { intros i s. by rewrite lookup_fmap fmap_Some=> -[? [/HB -> ->]]. }
   rewrite lft_vs_unfold; iDestruct "Hvs" as (n) "[Hcnt Hvs]".
-  iDestruct (big_sepS_filter_acc (⊂ κ) _ _ (dom _ I) with "Halive")
+  iDestruct (big_sepS_filter_acc (.⊂ κ) _ _ (dom _ I) with "Halive")
     as "[Halive Halive']".
   { intros κ'. rewrite elem_of_dom. eauto. }
   iApply fupd_trans. iApply fupd_mask_mono; first by apply union_subseteq_l.
   iMod ("Hvs" $! I with "[HI Halive Hbox Hbor] HP Hκ") as "(Hinv & HQ & Hcnt')".
   { rewrite lft_vs_inv_unfold. iFrame. rewrite /lft_bor_dead.
     iExists (dom _ B), P. rewrite !gset_to_gmap_dom -map_fmap_compose.
-    rewrite (map_fmap_ext _ ((1%Qp,) ∘ to_agree) B); last naive_solver.
+    rewrite (map_fmap_ext _ ((1%Qp,.) ∘ to_agree) B); last naive_solver.
     iFrame. }
   rewrite lft_vs_inv_unfold; iDestruct "Hinv" as "(?&HI&Halive)".
   iSpecialize ("Halive'" with "Halive").
@@ -100,7 +100,7 @@ Proof.
 Qed.
 
 Definition kill_set (I : gmap lft lft_names) (Λ : atomic_lft) : gset lft :=
-  filter (Λ ∈) (dom (gset lft) I).
+  filter (Λ ∈.) (dom (gset lft) I).
 
 Lemma elem_of_kill_set I Λ κ : κ ∈ kill_set I Λ ↔ Λ ∈ κ ∧ is_Some (I !! κ).
 Proof. by rewrite /kill_set elem_of_filter elem_of_dom. Qed.
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index f2acef14a2b36c11bb0ff4f08c955dba42c87633..19961dbf34a6f26f3037e38e22f240856ff683dc 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -74,7 +74,7 @@ Definition to_lft_stateR (b : bool) : lft_stateR :=
   if b then Cinl 1%Qp else Cinr ().
 Definition to_alftUR : gmap atomic_lft bool → alftUR := fmap to_lft_stateR.
 Definition to_ilftUR : gmap lft lft_names → ilftUR := fmap to_agree.
-Definition to_borUR : gmap slice_name bor_state → borUR := fmap ((1%Qp,) ∘ to_agree).
+Definition to_borUR : gmap slice_name bor_state → borUR := fmap ((1%Qp,.) ∘ to_agree).
 
 Section defs.
   Context `{!invG Σ, !lftG Σ}.
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index e3ab4f517363ad4aef0422d6c70983a7beab4c60..27368e2108de48c974e5cdfcb0fcd9afd71a2cdd 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -258,8 +258,8 @@ Instance lft_inhabited : Inhabited lft := _.
 Instance bor_idx_inhabited : Inhabited bor_idx := _.
 Instance lft_intersect_comm : Comm (A:=lft) eq (⊓) := _.
 Instance lft_intersect_assoc : Assoc (A:=lft) eq (⊓) := _.
-Instance lft_intersect_inj_1 κ : Inj eq eq (κ ⊓) := _.
-Instance lft_intersect_inj_2 κ : Inj eq eq (⊓ κ) := _.
+Instance lft_intersect_inj_1 κ : Inj eq eq (κ ⊓.) := _.
+Instance lft_intersect_inj_2 κ : Inj eq eq (.⊓ κ) := _.
 Instance lft_intersect_left_id : LeftId eq static (⊓) := _.
 Instance lft_intersect_right_id : RightId eq static (⊓) := _.
 
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 28fa316e225bcd7d14efa5f53bddb466ca6b3cc5..d0b9063fe1bfd144d3ec8bffba02c533bf3320fc 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -51,7 +51,7 @@ Section lft_contexts.
     - iDestruct "H" as "[Hq Hq']".
       iDestruct "Hq" as (κ0) "(% & Hq & #?)".
       iDestruct "Hq'" as (κ0') "(% & Hq' & #?)". simpl in *.
-      rewrite (inj ((lft_intersect_list κs) ⊓) κ0' κ0); last congruence.
+      rewrite (inj ((lft_intersect_list κs) ⊓.) κ0' κ0); last congruence.
       iExists κ0. by iFrame "∗%".
   Qed.
 
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 3f66f55948b63311a2b042189180f4eefef819cf..b563e6ebbe0e05238d694f52ef4f9d289a30571b 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -166,8 +166,8 @@ Section ofe.
   Instance type_dist : Dist type := type_dist'.
 
   Let T := prodO
-    (prodO natO (thread_id -d> list val -d> iProp Σ))
-    (lft -d> thread_id -d> loc -d> iProp Σ).
+    (prodO natO (thread_id -d> list val -d> iPropO Σ))
+    (lft -d> thread_id -d> loc -d> iPropO Σ).
   Let P (x : T) : Prop :=
     (∀ κ tid l, Persistent (x.2 κ tid l)) ∧
     (∀ tid vl, x.1.2 tid vl -∗ ⌜length vl = x.1.1⌝) ∧
@@ -231,7 +231,7 @@ Section ofe.
       st_dist' n ty1 ty2.
   Instance st_dist : Dist simple_type := st_dist'.
 
-  Definition st_unpack (ty : simple_type) : thread_id -d> list val -d> iProp Σ :=
+  Definition st_unpack (ty : simple_type) : thread_id -d> list val -d> iPropO Σ :=
     λ tid vl, ty.(ty_own) tid vl.
 
   Definition st_ofe_mixin : OfeMixin simple_type.