diff --git a/opam b/opam
index c223120ac77075f4838bd72f7141eebc9c743875..a6e6f20c99ea1ef7dc0e6ca03e50c058e5db2304 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-06-13.0.860bd8e4") | (= "dev") }
+  "coq-iris" { (= "dev.2019-06-18.2.e039d7c7") | (= "dev") }
 ]
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index 4ddbc2ab4425d1a11e4164cc1f27ef491e0747fe..61343b05857bb79ee92c0c39c11db14935014091 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -10,13 +10,13 @@ Set Default Proof Using "Type".
 Import uPred.
 
 Definition lock_stateR : cmraT :=
-  csumR (exclR unitC) natR.
+  csumR (exclR unitO) natR.
 
 Definition heapUR : ucmraT :=
-  gmapUR loc (prodR (prodR fracR lock_stateR) (agreeR valC)).
+  gmapUR loc (prodR (prodR fracR lock_stateR) (agreeR valO)).
 
 Definition heap_freeableUR : ucmraT :=
-  gmapUR block (prodR fracR (gmapR Z (exclR unitC))).
+  gmapUR block (prodR fracR (gmapR Z (exclR unitO))).
 
 Class heapG Σ := HeapG {
   heap_inG :> inG Σ (authR heapUR);
@@ -50,7 +50,7 @@ Section definitions.
   Definition heap_mapsto_vec (l : loc) (q : Qp) (vl : list val) : iProp Σ :=
     ([∗ list] i ↦ v ∈ vl, heap_mapsto (l +ₗ i) q v)%I.
 
-  Fixpoint inter (i0 : Z) (n : nat) : gmapR Z (exclR unitC) :=
+  Fixpoint inter (i0 : Z) (n : nat) : gmapR Z (exclR unitO) :=
     match n with O => ∅ | S n => <[i0 := Excl ()]>(inter (i0+1) n) end.
 
   Definition heap_freeable_def (l : loc) (q : Qp) (n: nat) : iProp Σ :=
diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index 09f0425297e1519070538623db6528e15cd2824a..6ce23b84649824ac722949ec7300794ae5454046 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -596,9 +596,9 @@ Defined.
 Instance expr_inhabited : Inhabited expr := populate (Lit LitPoison).
 Instance val_inhabited : Inhabited val := populate (LitV LitPoison).
 
-Canonical Structure stateC := leibnizC state.
-Canonical Structure valC := leibnizC val.
-Canonical Structure exprC := leibnizC expr.
+Canonical Structure stateO := leibnizO state.
+Canonical Structure valO := leibnizO val.
+Canonical Structure exprO := leibnizO expr.
 
 (** Language *)
 Lemma lrust_lang_mixin : EctxiLanguageMixin of_val to_val fill_item head_step.
diff --git a/theories/lang/lib/arc.v b/theories/lang/lib/arc.v
index a9c1c933e814776b459f3760af4bc56c532fe076..b257e89e6f4c8b88f841dde741dd94df9e96a680 100644
--- a/theories/lang/lib/arc.v
+++ b/theories/lang/lib/arc.v
@@ -103,11 +103,11 @@ Definition try_unwrap_full : val :=
 (* Not bundling heapG, as it may be shared with other users. *)
 
 (* See rc.v for understanding the structure of this CMRA.
-   The only additional thing is the [optionR (exclR unitC))], used to handle
+   The only additional thing is the [optionR (exclR unitO))], used to handle
    properly the locking mechanisme for the weak count. *)
 Definition arc_stR :=
-  prodUR (optionUR (csumR (prodR (prodR fracR positiveR) (optionR (exclR unitC)))
-                          (exclR unitC))) natUR.
+  prodUR (optionUR (csumR (prodR (prodR fracR positiveR) (optionR (exclR unitO)))
+                          (exclR unitO))) natUR.
 Class arcG Σ :=
   RcG :> inG Σ (authR arc_stR).
 Definition arcΣ : gFunctors := #[GFunctor (authR arc_stR)].
diff --git a/theories/lang/lib/spawn.v b/theories/lang/lib/spawn.v
index 3426ad9850d65353b978f03d7bdbda93156a1197..11340bc2c8ed554bcdc02c0089a46773afa80984 100644
--- a/theories/lang/lib/spawn.v
+++ b/theories/lang/lib/spawn.v
@@ -28,8 +28,8 @@ Definition join : val :=
       "join" ["c"].
 
 (** The CMRA & functor we need. *)
-Class spawnG Σ := SpawnG { spawn_tokG :> inG Σ (exclR unitC) }.
-Definition spawnΣ : gFunctors := #[GFunctor (exclR unitC)].
+Class spawnG Σ := SpawnG { spawn_tokG :> inG Σ (exclR unitO) }.
+Definition spawnΣ : gFunctors := #[GFunctor (exclR unitO)].
 
 Instance subG_spawnΣ {Σ} : subG spawnΣ Σ → spawnG Σ.
 Proof. solve_inG. Qed.
diff --git a/theories/lang/proofmode.v b/theories/lang/proofmode.v
index a1b3db3e1a85ef863601d8ab98f9845d350230d5..223518ceeb5c25ddc15c2f81fd9625ee8fe2f3ca 100644
--- a/theories/lang/proofmode.v
+++ b/theories/lang/proofmode.v
@@ -166,7 +166,7 @@ Qed.
 End heap.
 
 Tactic Notation "wp_apply" open_constr(lem) :=
-  iPoseProofCore lem as false true (fun H =>
+  iPoseProofCore lem as false (fun H =>
     lazymatch goal with
     | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
       reshape_expr e ltac:(fun K e' =>
diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index fe1429b756ff7c8a0f62cbf6b4057ecd2837b3a5..c169f25e05c5e05200bba09dbb85b8b42c622d87 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -20,7 +20,7 @@ Notation lft_intersect_list l := (foldr lft_intersect static l).
 
 Instance lft_inhabited : Inhabited lft := populate static.
 
-Canonical lftC := leibnizC lft.
+Canonical lftO := leibnizO lft.
 
 Section derived.
 Context `{!invG Σ, !lftG Σ}.
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 8342a18c3b160accea5d9bc8b5a0ee784940f08d..ede0dc16eb023979a3a9d4bbd1cff202ba1b1783 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -25,19 +25,19 @@ Inductive bor_state :=
   | Bor_in
   | Bor_open (q : frac)
   | Bor_rebor (κ : lft).
-Canonical bor_stateC := leibnizC bor_state.
+Canonical bor_stateO := leibnizO bor_state.
 
 Record lft_names := LftNames {
   bor_name : gname;
   cnt_name : gname;
   inh_name : gname
 }.
-Canonical lft_namesC := leibnizC lft_names.
+Canonical lft_namesO := leibnizO lft_names.
 
 Definition lft_stateR := csumR fracR unitR.
 Definition alftUR := gmapUR atomic_lft lft_stateR.
-Definition ilftUR := gmapUR lft (agreeR lft_namesC).
-Definition borUR := gmapUR slice_name (prodR fracR (agreeR bor_stateC)).
+Definition ilftUR := gmapUR lft (agreeR lft_namesO).
+Definition borUR := gmapUR slice_name (prodR fracR (agreeR bor_stateO)).
 Definition inhUR := gset_disjUR slice_name.
 
 Class lftG Σ := LftG {
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index 58c3ebe5a07fb7184027a1a11f8be57fa0bf9b46..7236c894918b6796482098af67b7c7abfb5a3524 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -18,7 +18,7 @@ Proof.
   { iModIntro. iExists A, I. by iFrame. }
   iMod (own_alloc (● 0 ⋅ ◯ 0)) as (γcnt) "[Hcnt Hcnt']"; first by apply auth_both_valid.
   iMod (own_alloc ((● ∅ ⋅ ◯ ∅) :auth (gmap slice_name
-      (frac * agree bor_stateC)))) as (γbor) "[Hbor Hbor']";
+      (frac * agree bor_stateO)))) as (γbor) "[Hbor Hbor']";
     first by apply auth_both_valid.
   iMod (own_alloc ((● ε) :auth (gset_disj slice_name)))
      as (γinh) "Hinh"; first by apply auth_auth_valid.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index d74d620b91d9be9806ef14a9c5054c5912816098..43a941772aacfa609549545fafff960131113351 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -8,7 +8,7 @@ From lrust.typing Require Import typing option.
 Set Default Proof Using "Type".
 
 Definition rc_stR :=
-  prodUR (optionUR (csumR (prodR fracR positiveR) (exclR unitC))) natUR.
+  prodUR (optionUR (csumR (prodR fracR positiveR) (exclR unitO))) natUR.
 Class rcG Σ :=
   RcG :> inG Σ (authR rc_stR).
 Definition rcΣ : gFunctors := #[GFunctor (authR rc_stR)].
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index b82faca971fd972523650f9c5c9a5bc669ba535c..0eb37efc77c23747683ed05bae3d3b6763205374 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -7,7 +7,7 @@ Set Default Proof Using "Type".
 
 Definition refcell_stR :=
   optionUR (prodR (prodR
-             (agreeR (prodC lftC boolC))
+             (agreeR (prodO lftO boolO))
              fracR)
              positiveR).
 Class refcellG Σ :=
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 92cd71816d62f1cb35f97c37970859ec56447b34..45a3c81c96eefd5b469b69e338650eb0ba525d9a 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -6,7 +6,7 @@ From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Definition rwlock_stR :=
-  optionUR (csumR (exclR unitC) (prodR (prodR (agreeR lftC) fracR) positiveR)).
+  optionUR (csumR (exclR unitO) (prodR (prodR (agreeR lftO) fracR) positiveR)).
 Class rwlockG Σ :=
   RwLockG :> inG Σ (authR rwlock_stR).
 Definition rwlockΣ : gFunctors := #[GFunctor (authR rwlock_stR)].
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 9f2a0c372d5710b87a217bd3435ab3cc8f6f22ca..3f66f55948b63311a2b042189180f4eefef819cf 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -165,9 +165,9 @@ Section ofe.
       type_dist' n ty1 ty2.
   Instance type_dist : Dist type := type_dist'.
 
-  Let T := prodC
-    (prodC natC (thread_id -c> list val -c> iProp Σ))
-    (lft -c> thread_id -c> loc -c> iProp Σ).
+  Let T := prodO
+    (prodO natO (thread_id -d> list val -d> iProp Σ))
+    (lft -d> thread_id -d> loc -d> iProp Σ).
   Let P (x : T) : Prop :=
     (∀ κ tid l, Persistent (x.2 κ tid l)) ∧
     (∀ tid vl, x.1.2 tid vl -∗ ⌜length vl = x.1.1⌝) ∧
@@ -188,7 +188,7 @@ Section ofe.
     - split; [by destruct 1|by intros [[??] ?]; constructor].
     - split; [by destruct 1|by intros [[??] ?]; constructor].
   Qed.
-  Canonical Structure typeC : ofeT := OfeT type type_ofe_mixin.
+  Canonical Structure typeO : ofeT := OfeT type type_ofe_mixin.
 
   Global Instance ty_size_ne n : Proper (dist n ==> eq) ty_size.
   Proof. intros ?? EQ. apply EQ. Qed.
@@ -206,7 +206,7 @@ Section ofe.
     Proper ((≡) ==> eq ==> eq ==> eq ==> (≡)) ty_shr.
   Proof. intros ?? EQ ??-> ??-> ??->. apply EQ. Qed.
 
-  Global Instance type_cofe : Cofe typeC.
+  Global Instance type_cofe : Cofe typeO.
   Proof.
     apply (iso_cofe_subtype' P type_pack type_unpack).
     - by intros [].
@@ -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 -c> list val -c> iProp Σ :=
+  Definition st_unpack (ty : simple_type) : thread_id -d> list val -d> iProp Σ :=
     λ tid vl, ty.(ty_own) tid vl.
 
   Definition st_ofe_mixin : OfeMixin simple_type.
@@ -240,7 +240,7 @@ Section ofe.
     - split; [by destruct 1|by constructor].
     - split; [by destruct 1|by constructor].
   Qed.
-  Canonical Structure stC : ofeT := OfeT simple_type st_ofe_mixin.
+  Canonical Structure stO : ofeT := OfeT simple_type st_ofe_mixin.
 
   Global Instance st_own_ne n :
     Proper (dist n ==> eq ==> eq ==> dist n) st_own.