diff --git a/opam b/opam
index 2f519a3b632082ab1618a2f1b93f60e59261dfd7..26435f35675ac60a97522e7c170d2c0d0290d7dc 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" { (= "3.2.0") | (= "dev") }
+  "coq-iris" { (= "dev.2019-09-19.3.aa7871c7") | (= "dev") }
   "coq-autosubst" { = "dev.coq86" }
 ]
diff --git a/theories/examples/stack/refinement.v b/theories/examples/stack/refinement.v
index c7315878307cf7aa0db17c26a9978ab1dc58e597..f9444e3e915b57381253032c569f978c341f0879 100644
--- a/theories/examples/stack/refinement.v
+++ b/theories/examples/stack/refinement.v
@@ -21,7 +21,7 @@ Section proof.
     iSplitL "H1"; eauto with iFrame.
   Qed.
 
-  Notation D := (locO -n> valO -n> iProp Σ).
+  Notation D := (locO -n> valO -n> iPropO Σ).
 
   Program Definition stack_link_pre (A : lrel Σ) : D -n> D := λne S v1 v2,
     (∃ w, (∃ q, v1 ↦{q} w) ∗
diff --git a/theories/experimental/helping/helping_stack.v b/theories/experimental/helping/helping_stack.v
index e0a3b693ff357dccbebe62b9277f0869310c13b1..376e0f9847cb262a4af763406a23fa422c108cc3 100644
--- a/theories/experimental/helping/helping_stack.v
+++ b/theories/experimental/helping/helping_stack.v
@@ -221,7 +221,7 @@ Section refinement.
   Local Instance oloc_to_val_inj : Inj (=) (=) oloc_to_val.
   Proof. intros [|][|]; simpl; congruence. Qed.
 
-  Local Notation D := (olocO -d> valO -d> iProp Σ).
+  Local Notation D := (olocO -d> valO -d> iPropO Σ).
 
   Definition stack_link_pre (A : lrel Σ) : D → D := λ S ol v2,
     match ol return _ with
diff --git a/theories/logic/model.v b/theories/logic/model.v
index 0c3cfc48876eaef02add9dde8d6ad29af7fbbf53..057ce90f36ee59cf9ea84e63bc85f16d2eda3c96 100644
--- a/theories/logic/model.v
+++ b/theories/logic/model.v
@@ -29,12 +29,13 @@ Section lrel_ofe.
   Instance lrel_equiv : Equiv (lrel Σ) := λ A B, ∀ w1 w2, A w1 w2 ≡ B w1 w2.
   Instance lrel_dist : Dist (lrel Σ) := λ n A B, ∀ w1 w2, A w1 w2 ≡{n}≡ B w1 w2.
   Lemma lrel_ofe_mixin : OfeMixin (lrel Σ).
-  Proof. by apply (iso_ofe_mixin (lrel_car : lrel Σ → (val -d> val -d> iProp Σ))). Qed.
+  Proof. by apply (iso_ofe_mixin (lrel_car : lrel Σ → (val -d> val -d> iPropO Σ))). Qed.
   Canonical Structure lrelC := OfeT (lrel Σ) lrel_ofe_mixin.
 
   Global Instance lrel_cofe : Cofe lrelC.
   Proof.
-    apply (iso_cofe_subtype' (λ A : val -d> val -d> iProp Σ, ∀ w1 w2, Persistent (A w1 w2)) (@LRel _) lrel_car)=>//.
+    apply (iso_cofe_subtype' (λ A : val -d> val -d> iPropO Σ,
+      ∀ w1 w2, Persistent (A w1 w2)) (@LRel _) lrel_car)=>//.
     - apply _.
     - apply limit_preserving_forall=> w1.
       apply limit_preserving_forall=> w2.
diff --git a/theories/logic/spec_rules.v b/theories/logic/spec_rules.v
index 2db07ac771eea6b8395da192a3096d1bb9f416ed..2849bfdef781cecedca5298ca345a9da2f8e136a 100644
--- a/theories/logic/spec_rules.v
+++ b/theories/logic/spec_rules.v
@@ -112,7 +112,7 @@ Section rules.
     { by eapply auth_update, prod_local_update_1,
          singleton_local_update, (exclusive_local_update _ (Excl (fill K #p))). }
     iExists p. iFrame. iApply "Hclose". iNext.
-    iExists (<[j:=fill K #p]> tp), (state_upd_used_proph_id ({[ p ]} ∪) σ).
+    iExists (<[j:=fill K #p]> tp), (state_upd_used_proph_id ({[ p ]} ∪.) σ).
     rewrite to_tpool_insert'; last eauto. iFrame. iPureIntro.
     eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
   Qed.