diff --git a/opam b/opam
index a26355d0974d3fd3fe588ccd6da438dcff5f2732..5888ae5e346f7207e49c55851feb987e28c07308 100644
--- a/opam
+++ b/opam
@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
 depends: [
-  "coq-iris" { (= "dev.2019-06-13.0.860bd8e4") | (= "dev") }
+  "coq-iris" { (= "dev.2019-06-18.2.e039d7c7") | (= "dev") }
   "coq-autosubst" { = "dev.coq86" }
 ]
diff --git a/theories/barrier/example_joining_existentials.v b/theories/barrier/example_joining_existentials.v
index 40cd79b36b6d4486dfaa5e9ebf2410701e87e814..0ed7746c94d6abf3b6c5f66fe497f864ad0490e1 100644
--- a/theories/barrier/example_joining_existentials.v
+++ b/theories/barrier/example_joining_existentials.v
@@ -6,16 +6,16 @@ From iris.proofmode Require Import tactics.
 From iris_examples.barrier Require Import proof specification.
 Set Default Proof Using "Type".
 
-Definition one_shotR (Σ : gFunctors) (F : cFunctor) :=
-  csumR (exclR unitC) (agreeR $ laterC $ F (iPreProp Σ) _).
+Definition one_shotR (Σ : gFunctors) (F : oFunctor) :=
+  csumR (exclR unitO) (agreeR $ laterO $ F (iPreProp Σ) _).
 Definition Pending {Σ F} : one_shotR Σ F := Cinl (Excl ()).
-Definition Shot {Σ} {F : cFunctor} (x : F (iProp Σ) _) : one_shotR Σ F :=
-  Cinr $ to_agree $ Next $ cFunctor_map F (iProp_fold, iProp_unfold) x.
+Definition Shot {Σ} {F : oFunctor} (x : F (iProp Σ) _) : one_shotR Σ F :=
+  Cinr $ to_agree $ Next $ oFunctor_map F (iProp_fold, iProp_unfold) x.
 
-Class oneShotG (Σ : gFunctors) (F : cFunctor) :=
+Class oneShotG (Σ : gFunctors) (F : oFunctor) :=
   one_shot_inG :> inG Σ (one_shotR Σ F).
-Definition oneShotΣ (F : cFunctor) : gFunctors :=
-  #[ GFunctor (csumRF (exclRF unitC) (agreeRF (â–¶ F))) ].
+Definition oneShotΣ (F : oFunctor) : gFunctors :=
+  #[ GFunctor (csumRF (exclRF unitO) (agreeRF (â–¶ F))) ].
 Instance subG_oneShotΣ {Σ F} : subG (oneShotΣ F) Σ → oneShotG Σ F.
 Proof. solve_inG. Qed.
 
@@ -59,12 +59,12 @@ Proof.
   iAssert (▷ (x ≡ x'))%I as "Hxx".
   { iCombine "Hγ" "Hγ'" as "Hγ2". iClear "Hγ Hγ'".
     rewrite own_valid csum_validI /= agree_validI agree_equivI bi.later_equivI /=.
-    rewrite -{2}[x]cFunctor_id -{2}[x']cFunctor_id.
-    assert (HF : cFunctor_map F (cid, cid) ≡ cFunctor_map F (iProp_fold (Σ:=Σ) ◎ iProp_unfold, iProp_fold (Σ:=Σ) ◎ iProp_unfold)).
+    rewrite -{2}[x]oFunctor_id -{2}[x']oFunctor_id.
+    assert (HF : oFunctor_map F (cid, cid) ≡ oFunctor_map F (iProp_fold (Σ:=Σ) ◎ iProp_unfold, iProp_fold (Σ:=Σ) ◎ iProp_unfold)).
     { apply ne_proper; first by apply _.
       by split; intro; simpl; symmetry; apply iProp_fold_unfold. }
     rewrite (HF x). rewrite (HF x').
-    rewrite !cFunctor_compose. iNext. by iRewrite "Hγ2". }
+    rewrite !oFunctor_compose. iNext. by iRewrite "Hγ2". }
   iNext. iRewrite -"Hxx" in "Hx'".
   iExists x; iFrame "Hγ". iApply (Ψ_join with "Hx Hx'").
 Qed.
diff --git a/theories/barrier/specification.v b/theories/barrier/specification.v
index 0dceb3e6f1f761e228d79d32686041e8b6274969..650e001176a3b5e1d3af6ca11454903e78dcdad8 100644
--- a/theories/barrier/specification.v
+++ b/theories/barrier/specification.v
@@ -18,7 +18,7 @@ Lemma barrier_spec (N : namespace) :
     (∀ l P Q, recv l (P ∗ Q) ={↑N}=> recv l P ∗ recv l Q) ∧
     (∀ l P Q, (P -∗ Q) -∗ recv l P -∗ recv l Q).
 Proof.
-  exists (λ l, CofeMor (recv N l)), (λ l, CofeMor (send N l)).
+  exists (λ l, OfeMor (recv N l)), (λ l, OfeMor (send N l)).
   split_and?; simpl.
   - iIntros (P) "!# _". iApply (newbarrier_spec _ P with "[]"); [done..|].
     iNext. eauto.
diff --git a/theories/concurrent_stacks/concurrent_stack1.v b/theories/concurrent_stacks/concurrent_stack1.v
index f471e164f8a1269d69af9db0f8d36c227f31abc2..2ce3dd95907cd3806e6ac7f611501f9c6b27531c 100644
--- a/theories/concurrent_stacks/concurrent_stack1.v
+++ b/theories/concurrent_stacks/concurrent_stack1.v
@@ -36,8 +36,8 @@ Section stacks.
     iIntros "H"; iDestruct "H" as (?) "[Hl Hl']"; iSplitL "Hl"; eauto.
   Qed.
 
-  Definition is_list_pre (P : val → iProp Σ) (F : val -c> iProp Σ) :
-     val -c> iProp Σ := λ v,
+  Definition is_list_pre (P : val → iProp Σ) (F : val -d> iProp Σ) :
+     val -d> iProp Σ := λ v,
     (v ≡ NONEV ∨ ∃ (l : loc) (h t : val), ⌜v ≡ SOMEV #l⌝ ∗ l ↦{-} (h, t)%V ∗ P h ∗ ▷ F t)%I.
 
   Local Instance is_list_contr (P : val → iProp Σ) : Contractive (is_list_pre P).
diff --git a/theories/concurrent_stacks/concurrent_stack2.v b/theories/concurrent_stacks/concurrent_stack2.v
index 7f11d03c2e9b672826d4f2918701f15a7d85265d..b916382218c00ecfd056e1195b3e2f368356bf56 100644
--- a/theories/concurrent_stacks/concurrent_stack2.v
+++ b/theories/concurrent_stacks/concurrent_stack2.v
@@ -246,8 +246,8 @@ Section stack_works.
     iIntros "H"; iDestruct "H" as (?) "[Hl Hl']"; iSplitL "Hl"; eauto.
   Qed.
 
-  Definition is_list_pre (P : val → iProp Σ) (F : val -c> iProp Σ) :
-     val -c> iProp Σ := λ v,
+  Definition is_list_pre (P : val → iProp Σ) (F : val -d> iProp Σ) :
+     val -d> iProp Σ := λ v,
     (v ≡ NONEV ∨ ∃ (l : loc) (h t : val), ⌜v ≡ SOMEV #l⌝ ∗ l ↦{-} (h, t)%V ∗ P h ∗ ▷ F t)%I.
 
   Local Instance is_list_contr (P : val → iProp Σ) : Contractive (is_list_pre P).
diff --git a/theories/hocap/cg_bag.v b/theories/hocap/cg_bag.v
index 758a7389639c5851b9ec372a0d0b68747c76ca8f..bd7014d1b131bfd50098f140d34223ad192aeb46 100644
--- a/theories/hocap/cg_bag.v
+++ b/theories/hocap/cg_bag.v
@@ -38,9 +38,9 @@ Definition popBag : val := λ: "b",
   release "l";;
   "v".
 
-Canonical Structure valmultisetC := leibnizC (gmultiset valC).
+Canonical Structure valmultisetO := leibnizO (gmultiset valO).
 Class bagG Σ := BagG
-{ bag_bagG :> inG Σ (prodR fracR (agreeR valmultisetC));
+{ bag_bagG :> inG Σ (prodR fracR (agreeR valmultisetO));
   lock_bagG :> lockG Σ
 }.
 
diff --git a/theories/hocap/concurrent_runners.v b/theories/hocap/concurrent_runners.v
index fbbbacd001869100fbc7533369dd16c231cecd95..7387613a2c2bef06e07351a0daeb334774295638 100644
--- a/theories/hocap/concurrent_runners.v
+++ b/theories/hocap/concurrent_runners.v
@@ -14,7 +14,7 @@ Set Default Proof Using "Type".
     SET_RES v = the result of the task has been computed and it is v
     FIN v = the task has been completed with the result v *)
 (* We use this RA to verify the Task.run() method *)
-Definition saR := csumR fracR (csumR (prodR fracR (agreeR valC)) (agreeR valC)).
+Definition saR := csumR fracR (csumR (prodR fracR (agreeR valO)) (agreeR valO)).
 Class saG Σ := { sa_inG :> inG Σ saR }.
 Definition INIT `{saG Σ} γ (q: Qp) := own γ (Cinl q%Qp).
 Definition SET_RES `{saG Σ} γ (q: Qp) (v: val) := own γ (Cinr (Cinl (q%Qp, to_agree v))).
@@ -189,7 +189,7 @@ Section contents.
   Ltac solve_proper ::= solve_proper_core ltac:(fun _ => simpl; auto_equiv).
 
   Program Definition pre_runner (γ : name Σ b) (P: val → iProp Σ) (Q: val → val → iProp Σ) :
-    (valC -n> iProp Σ) -n> (valC -n> iProp Σ) := λne R r,
+    (valO -n> iProp Σ) -n> (valO -n> iProp Σ) := λne R r,
     (∃ (body bag : val), ⌜r = (body, bag)%V⌝
      ∗ bagS b (N.@"bag") (λ x y, ∃ γ γ', isTask (body,x) γ γ' y P Q) γ bag
      ∗ ▷ ∀ r a: val, □ (R r ∗ P a -∗ WP body r a {{ v, Q a v }}))%I.
@@ -200,7 +200,7 @@ Section contents.
   Proof. unfold pre_runner. solve_contractive. Qed.
 
   Definition runner (γ: name Σ b) (P: val → iProp Σ) (Q: val → val → iProp Σ) :
-    valC -n> iProp Σ :=
+    valO -n> iProp Σ :=
     (fixpoint (pre_runner γ P Q))%I.
 
   Lemma runner_unfold γ r P Q :
diff --git a/theories/hocap/fg_bag.v b/theories/hocap/fg_bag.v
index 7f174c70b675def0850716333c53fd19787c5622..916c489f7e95f6fcf81b2bf5bf9a31515a62afe4 100644
--- a/theories/hocap/fg_bag.v
+++ b/theories/hocap/fg_bag.v
@@ -34,9 +34,9 @@ Definition popBag : val := rec: "pop" "b" :=
     else "pop" "b"
   end.
 
-Canonical Structure valmultisetC := leibnizC (gmultiset valC).
+Canonical Structure valmultisetO := leibnizO (gmultiset valO).
 Class bagG Σ := BagG
-{ bag_bagG :> inG Σ (prodR fracR (agreeR valmultisetC));
+{ bag_bagG :> inG Σ (prodR fracR (agreeR valmultisetO));
 }.
 
 (** Generic specification for the bag, using view shifts. *)
diff --git a/theories/hocap/lib/oneshot.v b/theories/hocap/lib/oneshot.v
index 24a7aa1bf63c6622bce4bb3609ee5d52ce417920..e4d20b6afb4233a04e51be481630ae00bc471de4 100644
--- a/theories/hocap/lib/oneshot.v
+++ b/theories/hocap/lib/oneshot.v
@@ -6,7 +6,7 @@ Set Default Proof Using "Type".
 
 (** We are going to need the oneshot RA to verify the
     Task.Join() method *)
-Definition oneshotR := csumR fracR (agreeR valC).
+Definition oneshotR := csumR fracR (agreeR valO).
 Class oneshotG Σ := { oneshot_inG :> inG Σ oneshotR }.
 Definition oneshotΣ : gFunctors := #[GFunctor oneshotR].
 Instance subG_oneshotΣ {Σ} : subG oneshotΣ Σ → oneshotG Σ.
diff --git a/theories/lecture_notes/coq_intro_example_2.v b/theories/lecture_notes/coq_intro_example_2.v
index 6e6ced292fa05655d85dc9d1cdeea3c1f993ace4..7d95642b1107125710ecb52342a80973fca3c395 100644
--- a/theories/lecture_notes/coq_intro_example_2.v
+++ b/theories/lecture_notes/coq_intro_example_2.v
@@ -59,12 +59,12 @@ Section monotone_counter.
    *)
 
   (* 
-     To tell Coq we wish to use such a discrete CMRA we use the constructor leibnizC.
+     To tell Coq we wish to use such a discrete CMRA we use the constructor leibnizO.
      This takes a Coq type and makes it an instance of an OFE (a step-indexed generalization of sets).
      This is not the place do describe Canonical Structures.
      A very good introduction is available at https://hal.inria.fr/hal-00816703v1/document 
   *)
-  Canonical Structure mcounterRAC := leibnizC mcounterRAT.
+  Canonical Structure mcounterRAC := leibnizO mcounterRAT.
 
   (* To make the type mcounterRAT into an RA we need an operation. This is
      defined in the standard way, except we use the typeclass Op so we can reuse
diff --git a/theories/lecture_notes/lists_guarded.v b/theories/lecture_notes/lists_guarded.v
index 04f333627c72c9244f0e82803deeaf539065a658..82e8c6beba0c50be0f22acffb8518cb9b2853ec8 100644
--- a/theories/lecture_notes/lists_guarded.v
+++ b/theories/lecture_notes/lists_guarded.v
@@ -46,7 +46,7 @@ Notation iProp := (iProp Σ).
   
 (* First we define the is_list representation predicate via a guarded fixed
    point of the functional is_list_pre. Note the use of the later modality. The
-   arrows -c> express that the arrow is an arrow in the category of COFE's,
+   arrows -d> express that the arrow is an arrow in the category of COFE's,
    i.e., it is a non-expansive function. To fully understand the meaning of this
    it is necessary to understand the model of Iris.
 
@@ -55,7 +55,7 @@ Notation iProp := (iProp Σ).
    but in more complex examples the domain of the predicate we are defining will
    not be a discrete type, and the condition will be meaningful and necessary.
 *)
-  Definition is_list_pre (Φ : val -c> list val -c> iProp): val -c> list val -c> iProp := λ hd xs,
+  Definition is_list_pre (Φ : val -d> list val -d> iProp): val -d> list val -d> iProp := λ hd xs,
     match xs with
       [] => ⌜hd = NONEV⌝
     | (x::xs) => (∃ (ℓ : loc) (hd' : val), ⌜hd = SOMEV #ℓ⌝ ∗ ℓ ↦ (x,hd') ∗ ▷ Φ hd' xs)
diff --git a/theories/lecture_notes/modular_incr.v b/theories/lecture_notes/modular_incr.v
index 2e56aa0a4e8badef8a6988543139d31ff341431e..7b756378dfc298c1a28abfa30a013059b6a82c1d 100644
--- a/theories/lecture_notes/modular_incr.v
+++ b/theories/lecture_notes/modular_incr.v
@@ -9,7 +9,7 @@ From iris.bi.lib Require Import fractional.
 
 From iris.heap_lang.lib Require Import par.
 
-Definition cntCmra : cmraT := (prodR fracR (agreeR (leibnizC Z))).
+Definition cntCmra : cmraT := (prodR fracR (agreeR (leibnizO Z))).
 
 Class cntG Σ := CntG { CntG_inG :> inG Σ cntCmra }.
 Definition cntΣ : gFunctors := #[GFunctor cntCmra ].
diff --git a/theories/logatom/conditional_increment/cinc.v b/theories/logatom/conditional_increment/cinc.v
index 7bd2e9a047de8f064f85286ae7e5fd21b458cec5..bb92592665c97b25116c3b0a9d679dd45cac564a 100644
--- a/theories/logatom/conditional_increment/cinc.v
+++ b/theories/logatom/conditional_increment/cinc.v
@@ -90,10 +90,10 @@ Definition cinc : val :=
 
 (** ** Proof setup *)
 
-Definition flagUR     := authR $ optionUR $ exclR boolC.
-Definition numUR      := authR $ optionUR $ exclR ZC.
-Definition tokenUR    := exclR unitC.
-Definition one_shotUR := csumR (exclR unitC) (agreeR unitC).
+Definition flagUR     := authR $ optionUR $ exclR boolO.
+Definition numUR      := authR $ optionUR $ exclR ZO.
+Definition tokenUR    := exclR unitO.
+Definition one_shotUR := csumR (exclR unitO) (agreeR unitO).
 
 Class cincG Σ := ConditionalIncrementG {
                      cinc_flagG     :> inG Σ flagUR;
diff --git a/theories/logatom/elimination_stack/hocap_spec.v b/theories/logatom/elimination_stack/hocap_spec.v
index 8db98bffcffbbff9932918380f554b7d4b0740ab..cda7ac91a3b0585b288fbfa7e7a18de803d7b8fe 100644
--- a/theories/logatom/elimination_stack/hocap_spec.v
+++ b/theories/logatom/elimination_stack/hocap_spec.v
@@ -138,10 +138,10 @@ auth invariant. *)
 
 (** The CMRA & functor we need. *)
 Class hocapG Σ := HocapG {
-  hocap_stateG :> inG Σ (authR (optionUR $ exclR (listC valC)));
+  hocap_stateG :> inG Σ (authR (optionUR $ exclR (listO valO)));
 }.
 Definition hocapΣ : gFunctors :=
-  #[GFunctor (exclR unitC); GFunctor (authR (optionUR $ exclR (listC valC)))].
+  #[GFunctor (exclR unitO); GFunctor (authR (optionUR $ exclR (listO valO)))].
 
 Instance subG_hocapΣ {Σ} : subG hocapΣ Σ → hocapG Σ.
 Proof. solve_inG. Qed.
diff --git a/theories/logatom/elimination_stack/stack.v b/theories/logatom/elimination_stack/stack.v
index 0c8562243d6502774ef8b19149ad6f42e24791c9..7b7aec1a4a48b156e5c4123375b95017e49948b7 100644
--- a/theories/logatom/elimination_stack/stack.v
+++ b/theories/logatom/elimination_stack/stack.v
@@ -13,11 +13,11 @@ heap. *)
 (** The CMRA & functor we need. *)
 (* Not bundling heapG, as it may be shared with other users. *)
 Class stackG Σ := StackG {
-  stack_tokG :> inG Σ (exclR unitC);
-  stack_stateG :> inG Σ (authR (optionUR $ exclR (listC valC)));
+  stack_tokG :> inG Σ (exclR unitO);
+  stack_stateG :> inG Σ (authR (optionUR $ exclR (listO valO)));
  }.
 Definition stackΣ : gFunctors :=
-  #[GFunctor (exclR unitC); GFunctor (authR (optionUR $ exclR (listC valC)))].
+  #[GFunctor (exclR unitO); GFunctor (authR (optionUR $ exclR (listO valO)))].
 
 Instance subG_stackΣ {Σ} : subG stackΣ Σ → stackG Σ.
 Proof. solve_inG. Qed.
diff --git a/theories/logatom/flat_combiner/atomic_sync.v b/theories/logatom/flat_combiner/atomic_sync.v
index bf1b078ea6911b47eaf4020393acf3fe69961d5b..c570a6b1c78a063c9714bf3f72bb1cd62cfada2c 100644
--- a/theories/logatom/flat_combiner/atomic_sync.v
+++ b/theories/logatom/flat_combiner/atomic_sync.v
@@ -6,7 +6,7 @@ From iris_examples.logatom.flat_combiner Require Import sync misc.
 
 (** The simple syncer spec in [sync.v] implies a logically atomic spec. *)
 
-Definition syncR := prodR fracR (agreeR valC). (* track the local knowledge of ghost state *)
+Definition syncR := prodR fracR (agreeR valO). (* track the local knowledge of ghost state *)
 Class syncG Σ := sync_tokG :> inG Σ syncR.
 Definition syncΣ : gFunctors := #[GFunctor (constRF syncR)].
 
@@ -15,8 +15,8 @@ Proof. solve_inG. Qed.
 
 Section atomic_sync.
   Context `{EqDecision A, !heapG Σ, !lockG Σ}.
-  Canonical AC := leibnizC A.
-  Context `{!inG Σ (prodR fracR (agreeR AC))}.
+  Canonical AO := leibnizO A.
+  Context `{!inG Σ (prodR fracR (agreeR AO))}.
 
   (* TODO: Rename and make opaque; the fact that this is a half should not be visible
            to the user. *)
@@ -56,7 +56,7 @@ Section atomic_sync.
     iSplitL "Hg2"; first done. iIntros "!#".
     iIntros (f). iApply wp_wand_r. iSplitR; first by iApply "Hsyncer".
     iIntros (f') "#Hsynced {Hsyncer}".
-    iAlways. iIntros (α β x) "#Hseq". change (ofe_car AC) with A.
+    iAlways. iIntros (α β x) "#Hseq". change (ofe_car AO) with A.
     iIntros (Φ') "?".
     (* TODO: Why can't I iApply "Hsynced"? *)
     iSpecialize ("Hsynced" $! _ Φ' x).
diff --git a/theories/logatom/flat_combiner/flat.v b/theories/logatom/flat_combiner/flat.v
index a4dd7247bb327da0e44456c8a2c5356999a2d1c7..fec42de26b8c76405fd71d9863cbd98e2a360888 100644
--- a/theories/logatom/flat_combiner/flat.v
+++ b/theories/logatom/flat_combiner/flat.v
@@ -46,7 +46,7 @@ Definition mk_flat : val :=
       let: "r" := loop "p" "s" "lk" in
       "r".
 
-Definition reqR := prodR fracR (agreeR valC). (* request x should be kept same *)
+Definition reqR := prodR fracR (agreeR valO). (* request x should be kept same *)
 Definition toks : Type := gname * gname * gname * gname * gname. (* a bunch of tokens to do state transition *)
 Class flatG Σ := FlatG {
   req_G :> inG Σ reqR;
diff --git a/theories/logatom/flat_combiner/misc.v b/theories/logatom/flat_combiner/misc.v
index b31ea9de467860acdd5d05b3f00f0bda884b7c72..411802921f6964c06cf236d4b7154597db288edd 100644
--- a/theories/logatom/flat_combiner/misc.v
+++ b/theories/logatom/flat_combiner/misc.v
@@ -20,7 +20,7 @@ Section lemmas.
 End lemmas.
 
 Section excl.
-  Context `{!inG Σ (exclR unitC)}.
+  Context `{!inG Σ (exclR unitO)}.
   Lemma excl_falso γ Q':
     own γ (Excl ()) ∗ own γ (Excl ()) ⊢ Q'.
   Proof.
diff --git a/theories/logatom/snapshot/atomic_snapshot.v b/theories/logatom/snapshot/atomic_snapshot.v
index 5e4b1a00b546f47c6d25d9f73cc53c6cd5794584..278cff3bec9c7205935fe33eae5e4507c43aa8bf 100644
--- a/theories/logatom/snapshot/atomic_snapshot.v
+++ b/theories/logatom/snapshot/atomic_snapshot.v
@@ -70,14 +70,14 @@ Definition read_with_proph : val :=
 
 (** The CMRA & functor we need. *)
 
-Definition timestampUR := gmapUR Z $ agreeR valC.
+Definition timestampUR := gmapUR Z $ agreeR valO.
 
 Class atomic_snapshotG Σ := AtomicSnapshotG {
-                                atomic_snapshot_stateG :> inG Σ $ authR $ optionUR $ exclR $ valC;
+                                atomic_snapshot_stateG :> inG Σ $ authR $ optionUR $ exclR $ valO;
                                 atomic_snapshot_timestampG :> inG Σ $ authR $ timestampUR
 }.
 Definition atomic_snapshotΣ : gFunctors :=
-  #[GFunctor (authR $ optionUR $ exclR $ valC); GFunctor (authR timestampUR)].
+  #[GFunctor (authR $ optionUR $ exclR $ valO); GFunctor (authR timestampUR)].
 
 Instance subG_atomic_snapshotΣ {Σ} : subG atomic_snapshotΣ Σ → atomic_snapshotG Σ.
 Proof. solve_inG. Qed.
diff --git a/theories/logatom/treiber2.v b/theories/logatom/treiber2.v
index 2501052d0396352e570cd87fb8ccdc97a88f1d3f..05ee4dc38ad6a2fcae148ec146eade2e64456cc7 100644
--- a/theories/logatom/treiber2.v
+++ b/theories/logatom/treiber2.v
@@ -58,10 +58,10 @@ Definition pop_stack : val :=
 (** * Definition of the required camera *************************************)
 
 Class stackG Σ := StackG {
-  stack_tokG :> inG Σ (authR (optionUR (exclR (listC valC)))) }.
+  stack_tokG :> inG Σ (authR (optionUR (exclR (listO valO)))) }.
 
 Definition stackΣ : gFunctors :=
-  #[GFunctor (authR (optionUR (exclR (listC valC))))].
+  #[GFunctor (authR (optionUR (exclR (listO valO))))].
 
 Instance subG_stackΣ {Σ} : subG stackΣ Σ → stackG Σ.
 Proof. solve_inG. Qed.
diff --git a/theories/logrel/F_mu/fundamental.v b/theories/logrel/F_mu/fundamental.v
index 52de92150d1e83edc7f4a02af9eb6392e8495d5a..c6a0c734218d582e055407628e715b0143266c4f 100644
--- a/theories/logrel/F_mu/fundamental.v
+++ b/theories/logrel/F_mu/fundamental.v
@@ -11,7 +11,7 @@ Notation "Γ ⊨ e : τ" := (log_typed Γ e τ) (at level 74, e, τ at next leve
 Section fundamental.
   Context `{irisG F_mu_lang Σ}.
 
-  Notation D := (valC -n> iProp Σ).
+  Notation D := (valO -n> iProp Σ).
 
   Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) constr(Hv) uconstr(Hp) :=
     iApply (wp_bind (fill[ctx]));
diff --git a/theories/logrel/F_mu/lang.v b/theories/logrel/F_mu/lang.v
index 3f901aa493decf671db51d66530cbffcfc71e7fd..a484ed711ac9e0b143ed7a3a63d2247064fb7d72 100644
--- a/theories/logrel/F_mu/lang.v
+++ b/theories/logrel/F_mu/lang.v
@@ -167,9 +167,9 @@ Module F_mu.
            fill_item_val, fill_item_no_val_inj, head_ctx_step_val.
   Qed.
 
-  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.
 End F_mu.
 
 (** Language *)
diff --git a/theories/logrel/F_mu/logrel.v b/theories/logrel/F_mu/logrel.v
index ff721cbbc3688bc2bfe676b557e8440972f992cf..e5d014c6faf68d37215c46cd872c84c5a1045d87 100644
--- a/theories/logrel/F_mu/logrel.v
+++ b/theories/logrel/F_mu/logrel.v
@@ -7,57 +7,57 @@ Import uPred.
 (** interp : is a unary logical relation. *)
 Section logrel.
   Context `{irisG F_mu_lang Σ}.
-  Notation D := (valC -n> iProp Σ).
+  Notation D := (valO -n> iProp Σ).
   Implicit Types Ï„i : D.
-  Implicit Types Δ : listC D.
-  Implicit Types interp : listC D → D.
+  Implicit Types Δ : listO D.
+  Implicit Types interp : listO D → D.
 
-  Program Definition ctx_lookup (x : var) : listC D -n> D := λne Δ,
+  Program Definition ctx_lookup (x : var) : listO D -n> D := λne Δ,
     from_option id (cconst True)%I (Δ !! x).
   Solve Obligations with solve_proper.
 
-  Definition interp_unit : listC D -n> D := λne Δ w, (⌜w = UnitV⌝)%I.
+  Definition interp_unit : listO D -n> D := λne Δ w, (⌜w = UnitV⌝)%I.
 
   Program Definition interp_prod
-      (interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ w,
+      (interp1 interp2 : listO D -n> D) : listO D -n> D := λne Δ w,
     (∃ w1 w2, ⌜w = PairV w1 w2⌝ ∧ interp1 Δ w1 ∧ interp2 Δ w2)%I.
   Solve Obligations with repeat intros ?; simpl; solve_proper.
 
   Program Definition interp_sum
-      (interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ w,
+      (interp1 interp2 : listO D -n> D) : listO D -n> D := λne Δ w,
     ((∃ w1, ⌜w = InjLV w1⌝ ∧ interp1 Δ w1) ∨ (∃ w2, ⌜w = InjRV w2⌝ ∧ interp2 Δ w2))%I.
   Solve Obligations with repeat intros ?; simpl; solve_proper.
 
   Program Definition interp_arrow
-      (interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ w,
+      (interp1 interp2 : listO D -n> D) : listO D -n> D := λne Δ w,
     (□ ∀ v, interp1 Δ v → WP App (# w) (# v) {{ interp2 Δ }})%I.
   Solve Obligations with repeat intros ?; simpl; solve_proper.
 
   Program Definition interp_forall
-      (interp : listC D -n> D) : listC D -n> D := λne Δ w,
+      (interp : listO D -n> D) : listO D -n> D := λne Δ w,
     (□ ∀ τi : D,
       ⌜∀ v, Persistent (τi v)⌝ → WP TApp (# w) {{ interp (τi :: Δ) }})%I.
   Solve Obligations with repeat intros ?; simpl; solve_proper.
 
   Definition interp_rec1
-      (interp : listC D -n> D) (Δ : listC D) (τi : D) : D := λne w,
+      (interp : listO D -n> D) (Δ : listO D) (τi : D) : D := λne w,
     (□ (∃ v, ⌜w = FoldV v⌝ ∧ ▷ interp (τi :: Δ) v))%I.
 
   Global Instance interp_rec1_contractive
-    (interp : listC D -n> D) (Δ : listC D) : Contractive (interp_rec1 interp Δ).
+    (interp : listO D -n> D) (Δ : listO D) : Contractive (interp_rec1 interp Δ).
   Proof. by solve_contractive. Qed.
 
-  Lemma fixpoint_interp_rec1_eq (interp : listC D -n> D) Δ x :
+  Lemma fixpoint_interp_rec1_eq (interp : listO D -n> D) Δ x :
     fixpoint (interp_rec1 interp Δ) x ≡ interp_rec1 interp Δ (fixpoint (interp_rec1 interp Δ)) x.
   Proof. exact: (fixpoint_unfold (interp_rec1 interp Δ) x). Qed.
 
-  Program Definition interp_rec (interp : listC D -n> D) : listC D -n> D := λne Δ,
+  Program Definition interp_rec (interp : listO D -n> D) : listO D -n> D := λne Δ,
     fixpoint (interp_rec1 interp Δ).
   Next Obligation.
     intros interp n Δ1 Δ2 HΔ; apply fixpoint_ne => τi w. solve_proper.
   Qed.
 
-  Fixpoint interp (Ï„ : type) : listC D -n> D :=
+  Fixpoint interp (Ï„ : type) : listO D -n> D :=
     match Ï„ return _ with
     | TUnit => interp_unit
     | TProd Ï„1 Ï„2 => interp_prod (interp Ï„1) (interp Ï„2)
@@ -70,11 +70,11 @@ Section logrel.
   Notation "⟦ τ ⟧" := (interp τ).
 
   Definition interp_env (Γ : list type)
-      (Δ : listC D) (vs : list val) : iProp Σ :=
+      (Δ : listO D) (vs : list val) : iProp Σ :=
     (⌜length Γ = length vs⌝ ∗ [∗] zip_with (λ τ, ⟦ τ ⟧ Δ) Γ vs)%I.
   Notation "⟦ Γ ⟧*" := (interp_env Γ).
 
-  Definition interp_expr (τ : type) (Δ : listC D) (e : expr) : iProp Σ :=
+  Definition interp_expr (τ : type) (Δ : listO D) (e : expr) : iProp Σ :=
     WP e {{ ⟦ τ ⟧ Δ }}%I.
 
   Class env_Persistent Δ :=
@@ -116,7 +116,7 @@ Section logrel.
     - rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl.
       { by rewrite !lookup_app_l. }
       (* FIXME: Ideally we wouldn't have to do this kinf of surgery. *)
-      change (bi_ofeC (uPredI (iResUR Σ))) with (uPredC (iResUR Σ)).
+      change (bi_ofeO (uPredI (iResUR Σ))) with (uPredO (iResUR Σ)).
       rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia.
     - intros w; simpl; properness; auto. apply (IHÏ„ (_ :: _)).
   Qed.
@@ -135,11 +135,11 @@ Section logrel.
     - rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl.
       { by rewrite !lookup_app_l. }
       (* FIXME: Ideally we wouldn't have to do this kinf of surgery. *)
-      change (bi_ofeC (uPredI (iResUR Σ))) with (uPredC (iResUR Σ)).
+      change (bi_ofeO (uPredI (iResUR Σ))) with (uPredO (iResUR Σ)).
       rewrite !lookup_app_r; [|lia ..].
       case EQ: (x - length Δ1) => [|n]; simpl.
       { symmetry. asimpl. apply (interp_weaken [] Δ1 Δ2 τ'). }
-      change (bi_ofeC (uPredI (iResUR Σ))) with (uPredC (iResUR Σ)).
+      change (bi_ofeO (uPredI (iResUR Σ))) with (uPredO (iResUR Σ)).
       rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia.
     - intros w; simpl; properness; auto. apply (IHÏ„ (_ :: _)).
   Qed.
diff --git a/theories/logrel/F_mu_ref/fundamental.v b/theories/logrel/F_mu_ref/fundamental.v
index 8fa60ef1650b67a130afa4167b3aa079a657235f..08187814b9aa62bfdffb45589d9b5cac9fe40435 100644
--- a/theories/logrel/F_mu_ref/fundamental.v
+++ b/theories/logrel/F_mu_ref/fundamental.v
@@ -10,7 +10,7 @@ Notation "Γ ⊨ e : τ" := (log_typed Γ e τ) (at level 74, e, τ at next leve
 
 Section fundamental.
   Context `{heapG Σ}.
-  Notation D := (valC -n> iProp Σ).
+  Notation D := (valO -n> iProp Σ).
 
   Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) constr(Hv) uconstr(Hp) :=
     iApply (wp_bind (fill [ctx]));
diff --git a/theories/logrel/F_mu_ref/fundamental_binary.v b/theories/logrel/F_mu_ref/fundamental_binary.v
index defc2f0813826ee9c7471ac345c54dcf76cafe9b..e4f49b9884764ce4f740b522c939c535f5c4f3d0 100644
--- a/theories/logrel/F_mu_ref/fundamental_binary.v
+++ b/theories/logrel/F_mu_ref/fundamental_binary.v
@@ -6,7 +6,7 @@ From iris_examples.logrel.F_mu_ref Require Import rules_binary.
 
 Section bin_log_def.
   Context `{heapG Σ,cfgSG Σ}.
-  Notation D := (prodC valC valC -n> iProp Σ).
+  Notation D := (prodO valO valO -n> iProp Σ).
 
   Definition bin_log_related (Γ : list type) (e e' : expr) (τ : type) :=
     ∀ Δ vvs (ρ : cfg F_mu_ref_lang), env_Persistent Δ →
@@ -19,9 +19,9 @@ Notation "Γ ⊨ e '≤log≤' e' : τ" :=
 
 Section fundamental.
   Context `{heapG Σ,cfgSG Σ}.
-  Notation D := (prodC valC valC -n> iProp Σ).
+  Notation D := (prodO valO valO -n> iProp Σ).
   Implicit Types e : expr.
-  Implicit Types Δ : listC D.
+  Implicit Types Δ : listO D.
   Hint Resolve to_of_val.
 
   Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) ident(w)
diff --git a/theories/logrel/F_mu_ref/lang.v b/theories/logrel/F_mu_ref/lang.v
index 596874275e030a1d0dd22909d83a93d079dd89b0..49e05629232d6782799036ac5026078311cce50f 100644
--- a/theories/logrel/F_mu_ref/lang.v
+++ b/theories/logrel/F_mu_ref/lang.v
@@ -214,9 +214,9 @@ Module F_mu_ref.
            fill_item_val, fill_item_no_val_inj, head_ctx_step_val.
   Qed.
 
-  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.
 End F_mu_ref.
 
 Canonical Structure F_mu_ref_ectxi_lang := EctxiLanguage F_mu_ref.lang_mixin.
diff --git a/theories/logrel/F_mu_ref/logrel.v b/theories/logrel/F_mu_ref/logrel.v
index 35dc3f0f08e3df3ea1d0fb22e17d03cb3089a8c1..60fd607995d40efbc82724d4c422afb606bc0cca 100644
--- a/theories/logrel/F_mu_ref/logrel.v
+++ b/theories/logrel/F_mu_ref/logrel.v
@@ -9,52 +9,52 @@ Definition logN : namespace := nroot .@ "logN".
 (** interp : is a unary logical relation. *)
 Section logrel.
   Context `{heapG Σ}.
-  Notation D := (valC -n> iProp Σ).
+  Notation D := (valO -n> iProp Σ).
   Implicit Types Ï„i : D.
-  Implicit Types Δ : listC D.
-  Implicit Types interp : listC D → D.
+  Implicit Types Δ : listO D.
+  Implicit Types interp : listO D → D.
 
-  Program Definition ctx_lookup (x : var) : listC D -n> D := λne Δ,
+  Program Definition ctx_lookup (x : var) : listO D -n> D := λne Δ,
     from_option id (cconst True)%I (Δ !! x).
   Solve Obligations with solve_proper.
 
-  Definition interp_unit : listC D -n> D := λne Δ w, ⌜w = UnitV⌝%I.
+  Definition interp_unit : listO D -n> D := λne Δ w, ⌜w = UnitV⌝%I.
 
   Program Definition interp_prod
-      (interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ w,
+      (interp1 interp2 : listO D -n> D) : listO D -n> D := λne Δ w,
     (∃ w1 w2, ⌜w = PairV w1 w2⌝ ∧ interp1 Δ w1 ∧ interp2 Δ w2)%I.
   Solve Obligations with repeat intros ?; simpl; solve_proper.
 
   Program Definition interp_sum
-      (interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ w,
+      (interp1 interp2 : listO D -n> D) : listO D -n> D := λne Δ w,
     ((∃ w1, ⌜w = InjLV w1⌝ ∧ interp1 Δ w1) ∨ (∃ w2, ⌜w = InjRV w2⌝ ∧ interp2 Δ w2))%I.
   Solve Obligations with repeat intros ?; simpl; solve_proper.
 
   Program Definition interp_arrow
-      (interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ w,
+      (interp1 interp2 : listO D -n> D) : listO D -n> D := λne Δ w,
     (□ ∀ v, interp1 Δ v → WP App (# w) (# v) {{ interp2 Δ }})%I.
   Solve Obligations with repeat intros ?; simpl; solve_proper.
 
   Program Definition interp_forall
-      (interp : listC D -n> D) : listC D -n> D := λne Δ w,
+      (interp : listO D -n> D) : listO D -n> D := λne Δ w,
     (□ ∀ τi : D,
       ⌜(∀ v, Persistent (τi v))⌝ → WP TApp (# w) {{ interp (τi :: Δ) }})%I.
   Solve Obligations with repeat intros ?; simpl; solve_proper.
 
   Definition interp_rec1
-      (interp : listC D -n> D) (Δ : listC D) (τi : D) : D := λne w,
+      (interp : listO D -n> D) (Δ : listO D) (τi : D) : D := λne w,
     (□ (∃ v, ⌜w = FoldV v⌝ ∧ ▷ interp (τi :: Δ) v))%I.
 
   Global Instance interp_rec1_contractive
-    (interp : listC D -n> D) (Δ : listC D) : Contractive (interp_rec1 interp Δ).
+    (interp : listO D -n> D) (Δ : listO D) : Contractive (interp_rec1 interp Δ).
   Proof. by solve_contractive. Qed.
 
 
-  Lemma fixpoint_interp_rec1_eq (interp : listC D -n> D) Δ x :
+  Lemma fixpoint_interp_rec1_eq (interp : listO D -n> D) Δ x :
     fixpoint (interp_rec1 interp Δ) x ≡ interp_rec1 interp Δ (fixpoint (interp_rec1 interp Δ)) x.
   Proof. exact: (fixpoint_unfold (interp_rec1 interp Δ) x). Qed.
 
-  Program Definition interp_rec (interp : listC D -n> D) : listC D -n> D := λne Δ,
+  Program Definition interp_rec (interp : listO D -n> D) : listO D -n> D := λne Δ,
     fixpoint (interp_rec1 interp Δ).
   Next Obligation.
     intros interp n Δ1 Δ2 HΔ; apply fixpoint_ne => τi w. solve_proper.
@@ -65,11 +65,11 @@ Section logrel.
   Solve Obligations with solve_proper.
 
   Program Definition interp_ref
-      (interp : listC D -n> D) : listC D -n> D := λne Δ w,
+      (interp : listO D -n> D) : listO D -n> D := λne Δ w,
     (∃ l, ⌜w = LocV l⌝ ∧ inv (logN .@ l) (interp_ref_inv l (interp Δ)))%I.
   Solve Obligations with solve_proper.
 
-  Fixpoint interp (Ï„ : type) : listC D -n> D :=
+  Fixpoint interp (Ï„ : type) : listO D -n> D :=
     match Ï„ return _ with
     | TUnit => interp_unit
     | TProd Ï„1 Ï„2 => interp_prod (interp Ï„1) (interp Ï„2)
@@ -83,11 +83,11 @@ Section logrel.
   Notation "⟦ τ ⟧" := (interp τ).
 
   Definition interp_env (Γ : list type)
-      (Δ : listC D) (vs : list val) : iProp Σ :=
+      (Δ : listO D) (vs : list val) : iProp Σ :=
     (⌜length Γ = length vs⌝ ∗ [∗] zip_with (λ τ, ⟦ τ ⟧ Δ) Γ vs)%I.
   Notation "⟦ Γ ⟧*" := (interp_env Γ).
 
-  Definition interp_expr (τ : type) (Δ : listC D) (e : expr) : iProp Σ :=
+  Definition interp_expr (τ : type) (Δ : listO D) (e : expr) : iProp Σ :=
     WP e {{ ⟦ τ ⟧ Δ }}%I.
 
   Class env_Persistent Δ :=
@@ -129,7 +129,7 @@ Section logrel.
     - rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl.
       { by rewrite !lookup_app_l. }
       (* FIXME: Ideally we wouldn't have to do this kinf of surgery. *)
-      change (bi_ofeC (uPredI (iResUR Σ))) with (uPredC (iResUR Σ)).
+      change (bi_ofeO (uPredI (iResUR Σ))) with (uPredO (iResUR Σ)).
       rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia.
     - intros w; simpl; properness; auto. apply (IHÏ„ (_ :: _)).
     - intros w; simpl; properness; auto. by apply IHÏ„.
@@ -149,11 +149,11 @@ Section logrel.
     - rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl.
       { by rewrite !lookup_app_l. }
       (* FIXME: Ideally we wouldn't have to do this kinf of surgery. *)
-      change (bi_ofeC (uPredI (iResUR Σ))) with (uPredC (iResUR Σ)).
+      change (bi_ofeO (uPredI (iResUR Σ))) with (uPredO (iResUR Σ)).
       rewrite !lookup_app_r; [|lia ..].
       case EQ: (x - length Δ1) => [|n]; simpl.
       { symmetry. asimpl. apply (interp_weaken [] Δ1 Δ2 τ'). }
-      change (bi_ofeC (uPredI (iResUR Σ))) with (uPredC (iResUR Σ)).
+      change (bi_ofeO (uPredI (iResUR Σ))) with (uPredO (iResUR Σ)).
       rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia.
     - intros w; simpl; properness; auto. apply (IHÏ„ (_ :: _)).
     - intros w; simpl; properness; auto. by apply IHÏ„.
diff --git a/theories/logrel/F_mu_ref/logrel_binary.v b/theories/logrel/F_mu_ref/logrel_binary.v
index 48908fe5245b3f61a55eed82325b27ee87f6e67f..1f24a7efa5b280e8f1a3fd76174d27f36eb1447a 100644
--- a/theories/logrel/F_mu_ref/logrel_binary.v
+++ b/theories/logrel/F_mu_ref/logrel_binary.v
@@ -25,12 +25,12 @@ Definition logN : namespace := nroot .@ "logN".
 (** interp : is a unary logical relation. *)
 Section logrel.
   Context `{heapG Σ, cfgSG Σ}.
-  Notation D := (prodC valC valC -n> iProp Σ).
+  Notation D := (prodO valO valO -n> iProp Σ).
   Implicit Types Ï„i : D.
-  Implicit Types Δ : listC D.
-  Implicit Types interp : listC D → D.
+  Implicit Types Δ : listO D.
+  Implicit Types interp : listO D → D.
 
-  Definition interp_expr (τi : listC D -n> D) (Δ : listC D)
+  Definition interp_expr (τi : listO D -n> D) (Δ : listO D)
       (ee : expr * expr) : iProp Σ := (∀ K,
     ⤇ fill K (ee.2) →
     WP ee.1 {{ v, ∃ v', ⤇ fill K (of_val v') ∗ τi Δ (v, v') }})%I.
@@ -38,28 +38,28 @@ Section logrel.
     Proper (dist n ==> dist n ==> (=) ==> dist n) interp_expr.
   Proof. solve_proper. Qed.
 
-  Program Definition ctx_lookup (x : var) : listC D -n> D := λne Δ,
+  Program Definition ctx_lookup (x : var) : listO D -n> D := λne Δ,
     from_option id (cconst True)%I (Δ !! x).
   Solve Obligations with solve_proper.
 
-  Program Definition interp_unit : listC D -n> D := λne Δ ww,
+  Program Definition interp_unit : listO D -n> D := λne Δ ww,
     (⌜ww.1 = UnitV⌝ ∧ ⌜ww.2 = UnitV⌝)%I.
   Solve Obligations with solve_proper_alt.
 
   Program Definition interp_prod
-      (interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ ww,
+      (interp1 interp2 : listO D -n> D) : listO D -n> D := λne Δ ww,
     (∃ vv1 vv2, ⌜ww = (PairV (vv1.1) (vv2.1), PairV (vv1.2) (vv2.2))⌝ ∧
                 interp1 Δ vv1 ∧ interp2 Δ vv2)%I.
   Solve Obligations with repeat intros ?; simpl; auto_equiv.
 
   Program Definition interp_sum
-      (interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ ww,
+      (interp1 interp2 : listO D -n> D) : listO D -n> D := λne Δ ww,
     ((∃ vv, ⌜ww = (InjLV (vv.1), InjLV (vv.2))⌝ ∧ interp1 Δ vv) ∨
      (∃ vv, ⌜ww = (InjRV (vv.1), InjRV (vv.2))⌝ ∧ interp2 Δ vv))%I.
   Solve Obligations with repeat intros ?; simpl; auto_equiv.
 
   Program Definition interp_arrow
-          (interp1 interp2 : listC D -n> D) : listC D -n> D :=
+          (interp1 interp2 : listO D -n> D) : listO D -n> D :=
     λne Δ ww,
     (□ ∀ vv, interp1 Δ vv →
              interp_expr
@@ -68,7 +68,7 @@ Section logrel.
   Solve Obligations with repeat intros ?; simpl; auto_equiv.
 
   Program Definition interp_forall
-      (interp : listC D -n> D) : listC D -n> D := λne Δ ww,
+      (interp : listO D -n> D) : listO D -n> D := λne Δ ww,
     (□ ∀ τi,
           ⌜∀ ww, Persistent (τi ww)⌝ →
           interp_expr
@@ -76,19 +76,19 @@ Section logrel.
   Solve Obligations with repeat intros ?; simpl; auto_equiv.
 
   Program Definition interp_rec1
-      (interp : listC D -n> D) (Δ : listC D) (τi : D) : D := λne ww,
+      (interp : listO D -n> D) (Δ : listO D) (τi : D) : D := λne ww,
     (□ ∃ vv, ⌜ww = (FoldV (vv.1), FoldV (vv.2))⌝ ∧ ▷ interp (τi :: Δ) vv)%I.
   Solve Obligations with repeat intros ?; simpl; auto_equiv.
 
   Global Instance interp_rec1_contractive
-    (interp : listC D -n> D) (Δ : listC D) : Contractive (interp_rec1 interp Δ).
+    (interp : listO D -n> D) (Δ : listO D) : Contractive (interp_rec1 interp Δ).
   Proof. by solve_contractive. Qed.
 
-  Lemma fixpoint_interp_rec1_eq (interp : listC D -n> D) Δ x :
+  Lemma fixpoint_interp_rec1_eq (interp : listO D -n> D) Δ x :
     fixpoint (interp_rec1 interp Δ) x ≡ interp_rec1 interp Δ (fixpoint (interp_rec1 interp Δ)) x.
   Proof. exact: (fixpoint_unfold (interp_rec1 interp Δ) x). Qed.
 
-  Program Definition interp_rec (interp : listC D -n> D) : listC D -n> D := λne Δ,
+  Program Definition interp_rec (interp : listO D -n> D) : listO D -n> D := λne Δ,
     fixpoint (interp_rec1 interp Δ).
   Next Obligation.
     intros interp n Δ1 Δ2 HΔ; apply fixpoint_ne => τi ww. solve_proper.
@@ -99,12 +99,12 @@ Section logrel.
   Solve Obligations with repeat intros ?; simpl; auto_equiv.
 
   Program Definition interp_ref
-      (interp : listC D -n> D) : listC D -n> D := λne Δ ww,
+      (interp : listO D -n> D) : listO D -n> D := λne Δ ww,
     (∃ ll, ⌜ww = (LocV (ll.1), LocV (ll.2))⌝ ∧
            inv (logN .@ ll) (interp_ref_inv ll (interp Δ)))%I.
   Solve Obligations with repeat intros ?; simpl; auto_equiv.
 
-  Fixpoint interp (Ï„ : type) : listC D -n> D :=
+  Fixpoint interp (Ï„ : type) : listO D -n> D :=
     match Ï„ return _ with
     | TUnit => interp_unit
     | TProd Ï„1 Ï„2 => interp_prod (interp Ï„1) (interp Ï„2)
@@ -118,7 +118,7 @@ Section logrel.
   Notation "⟦ τ ⟧" := (interp τ).
 
   Definition interp_env (Γ : list type)
-      (Δ : listC D) (vvs : list (val * val)) : iProp Σ :=
+      (Δ : listO D) (vvs : list (val * val)) : iProp Σ :=
     (⌜length Γ = length vvs⌝ ∗ [∗] zip_with (λ τ, ⟦ τ ⟧ Δ) Γ vvs)%I.
   Notation "⟦ Γ ⟧*" := (interp_env Γ).
 
@@ -162,7 +162,7 @@ Section logrel.
     - rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl.
       { by rewrite !lookup_app_l. }
       (* FIXME: Ideally we wouldn't have to do this kinf of surgery. *)
-      change (bi_ofeC (uPredI (iResUR Σ))) with (uPredC (iResUR Σ)).
+      change (bi_ofeO (uPredI (iResUR Σ))) with (uPredO (iResUR Σ)).
       rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia.
     - unfold interp_expr.
       intros ww; simpl; properness; auto. by apply (IHÏ„ (_ :: _)).
@@ -183,11 +183,11 @@ Section logrel.
     - rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl.
       { by rewrite !lookup_app_l. }
       (* FIXME: Ideally we wouldn't have to do this kinf of surgery. *)
-      change (bi_ofeC (uPredI (iResUR Σ))) with (uPredC (iResUR Σ)).
+      change (bi_ofeO (uPredI (iResUR Σ))) with (uPredO (iResUR Σ)).
       rewrite !lookup_app_r; [|lia ..].
       case EQ: (x - length Δ1) => [|n]; simpl.
       { symmetry. asimpl. apply (interp_weaken [] Δ1 Δ2 τ'). }
-      change (bi_ofeC (uPredI (iResUR Σ))) with (uPredC (iResUR Σ)).
+      change (bi_ofeO (uPredI (iResUR Σ))) with (uPredO (iResUR Σ)).
       rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia.
     - unfold interp_expr.
       intros ww; simpl; properness; auto. apply (IHÏ„ (_ :: _)).
diff --git a/theories/logrel/F_mu_ref/rules_binary.v b/theories/logrel/F_mu_ref/rules_binary.v
index 57b846f274e361d2a86aeacc40962ea8bcaf14c8..11b7499aa7ee500498758be85d5544d4cc2f0039 100644
--- a/theories/logrel/F_mu_ref/rules_binary.v
+++ b/theories/logrel/F_mu_ref/rules_binary.v
@@ -7,7 +7,7 @@ Import uPred.
 Definition specN := nroot .@ "spec".
 
 (** The CMRA for the heap of the specification. *)
-Definition cfgUR := prodUR (optionUR (exclR exprC)) (gen_heapUR loc val).
+Definition cfgUR := prodUR (optionUR (exclR exprO)) (gen_heapUR loc val).
 
 (** The CMRA for the thread pool. *)
 Class cfgSG Σ := CFGSG { cfg_inG :> inG Σ (authR cfgUR); cfg_name : gname }.
diff --git a/theories/logrel/F_mu_ref_conc/examples/counter.v b/theories/logrel/F_mu_ref_conc/examples/counter.v
index 7c4eaa7562228113f3a3b1f12f065bc0004c9418..2f43b80ff66d286f0d1bef8cc00b34411a8b28c3 100644
--- a/theories/logrel/F_mu_ref_conc/examples/counter.v
+++ b/theories/logrel/F_mu_ref_conc/examples/counter.v
@@ -35,8 +35,8 @@ Definition FG_counter : expr :=
 Section CG_Counter.
   Context `{heapIG Σ, cfgSG Σ}.
 
-  Notation D := (prodC valC valC -n> iProp Σ).
-  Implicit Types Δ : listC D.
+  Notation D := (prodO valO valO -n> iProp Σ).
+  Implicit Types Δ : listO D.
 
   (* Coarse-grained increment *)
   Lemma CG_increment_type x Γ :
diff --git a/theories/logrel/F_mu_ref_conc/examples/stack/refinement.v b/theories/logrel/F_mu_ref_conc/examples/stack/refinement.v
index 998a8e729e2233d3a3a4ee7ea8ff555c24e2fb6b..93fbed2850492b4ee4b80e31cc53f5b8d5c86225 100644
--- a/theories/logrel/F_mu_ref_conc/examples/stack/refinement.v
+++ b/theories/logrel/F_mu_ref_conc/examples/stack/refinement.v
@@ -10,8 +10,8 @@ Definition stackN : namespace := nroot .@ "stack".
 
 Section Stack_refinement.
   Context `{heapIG Σ, cfgSG Σ, inG Σ (authR stackUR)}.
-  Notation D := (prodC valC valC -n> iProp Σ).
-  Implicit Types Δ : listC D.
+  Notation D := (prodO valO valO -n> iProp Σ).
+  Implicit Types Δ : listO D.
 
   Lemma FG_CG_counter_refinement :
     [] ⊨ FG_stack ≤log≤ CG_stack : TForall (TProd (TProd
diff --git a/theories/logrel/F_mu_ref_conc/examples/stack/stack_rules.v b/theories/logrel/F_mu_ref_conc/examples/stack/stack_rules.v
index 99b1bb001ff0b0273c6d8a17060ae567dc85a905..7607df63de322c6c53900bbc5ed80b73a3ea62a5 100644
--- a/theories/logrel/F_mu_ref_conc/examples/stack/stack_rules.v
+++ b/theories/logrel/F_mu_ref_conc/examples/stack/stack_rules.v
@@ -5,7 +5,7 @@ Import uPred.
 From iris.algebra Require deprecated.
 Import deprecated.dec_agree.
 
-Definition stackUR : ucmraT := gmapUR loc (agreeR valC).
+Definition stackUR : ucmraT := gmapUR loc (agreeR valO).
 
 Class stackG Σ :=
   StackG { stack_inG :> inG Σ (authR stackUR); stack_name : gname }.
@@ -17,7 +17,7 @@ Notation "l ↦ˢᵗᵏ v" := (stack_mapsto l v) (at level 20) : bi_scope.
 
 Section Rules.
   Context `{stackG Σ}.
-  Notation D := (prodC valC valC -n> iProp Σ).
+  Notation D := (prodO valO valO -n> iProp Σ).
 
   Global Instance stack_mapsto_persistent l v : Persistent (l ↦ˢᵗᵏ v).
   Proof. apply _. Qed.
diff --git a/theories/logrel/F_mu_ref_conc/fundamental_binary.v b/theories/logrel/F_mu_ref_conc/fundamental_binary.v
index b683aa59d3949624daa9fe8a704b36d61fe752d6..260f457f25904e0ea04e215fa09c507b6b484e38 100644
--- a/theories/logrel/F_mu_ref_conc/fundamental_binary.v
+++ b/theories/logrel/F_mu_ref_conc/fundamental_binary.v
@@ -6,7 +6,7 @@ From iris.program_logic Require Export lifting.
 
 Section bin_log_def.
   Context `{heapIG Σ, cfgSG Σ}.
-  Notation D := (prodC valC valC -n> iProp Σ).
+  Notation D := (prodO valO valO -n> iProp Σ).
 
   Definition bin_log_related (Γ : list type) (e e' : expr) (τ : type) := ∀ Δ vvs,
     env_Persistent Δ →
@@ -19,9 +19,9 @@ Notation "Γ ⊨ e '≤log≤' e' : τ" :=
 
 Section fundamental.
   Context `{heapIG Σ, cfgSG Σ}.
-  Notation D := (prodC valC valC -n> iProp Σ).
+  Notation D := (prodO valO valO -n> iProp Σ).
   Implicit Types e : expr.
-  Implicit Types Δ : listC D.
+  Implicit Types Δ : listO D.
   Hint Resolve to_of_val.
 
   Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) ident(w)
diff --git a/theories/logrel/F_mu_ref_conc/fundamental_unary.v b/theories/logrel/F_mu_ref_conc/fundamental_unary.v
index 97fa81ba433ba487eae6bcec05a259b87593dd6a..e79b8a7351b60793496016dc8f06823ba9709212 100644
--- a/theories/logrel/F_mu_ref_conc/fundamental_unary.v
+++ b/theories/logrel/F_mu_ref_conc/fundamental_unary.v
@@ -11,7 +11,7 @@ Notation "Γ ⊨ e : τ" := (log_typed Γ e τ) (at level 74, e, τ at next leve
 
 Section typed_interp.
   Context `{heapIG Σ}.
-  Notation D := (valC -n> iProp Σ).
+  Notation D := (valO -n> iProp Σ).
 
   Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) constr(Hv) uconstr(Hp) :=
     iApply (wp_bind (fill [ctx]));
diff --git a/theories/logrel/F_mu_ref_conc/lang.v b/theories/logrel/F_mu_ref_conc/lang.v
index f852b58c5bbfe4cd6f64b50bce19a58145ea26f9..274441f4ec8ce318c920a1ca5954f648ae8c88c6 100644
--- a/theories/logrel/F_mu_ref_conc/lang.v
+++ b/theories/logrel/F_mu_ref_conc/lang.v
@@ -303,9 +303,9 @@ Module F_mu_ref_conc.
            fill_item_val, fill_item_no_val_inj, head_ctx_step_val.
   Qed.
 
-  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.
 End F_mu_ref_conc.
 
 Canonical Structure F_mu_ref_conc_ectxi_lang :=
diff --git a/theories/logrel/F_mu_ref_conc/logrel_binary.v b/theories/logrel/F_mu_ref_conc/logrel_binary.v
index 469776613373e6a46e1b106240c4ff2de1c1e374..cdbb64c6be5a4a52698d774a696f1a203ff02e68 100644
--- a/theories/logrel/F_mu_ref_conc/logrel_binary.v
+++ b/theories/logrel/F_mu_ref_conc/logrel_binary.v
@@ -28,12 +28,12 @@ Definition logN : namespace := nroot .@ "logN".
 (** interp : is a unary logical relation. *)
 Section logrel.
   Context `{heapIG Σ, cfgSG Σ}.
-  Notation D := (prodC valC valC -n> iProp Σ).
+  Notation D := (prodO valO valO -n> iProp Σ).
   Implicit Types Ï„i : D.
-  Implicit Types Δ : listC D.
-  Implicit Types interp : listC D → D.
+  Implicit Types Δ : listO D.
+  Implicit Types interp : listO D → D.
 
-  Definition interp_expr (τi : listC D -n> D) (Δ : listC D)
+  Definition interp_expr (τi : listO D -n> D) (Δ : listO D)
       (ee : expr * expr) : iProp Σ := (∀ j K,
     j ⤇ fill K (ee.2) →
     WP ee.1 {{ v, ∃ v', j ⤇ fill K (of_val v') ∗ τi Δ (v, v') }})%I.
@@ -41,35 +41,35 @@ Section logrel.
     Proper (dist n ==> dist n ==> (=) ==> dist n) interp_expr.
   Proof. unfold interp_expr; solve_proper. Qed.
 
-  Program Definition ctx_lookup (x : var) : listC D -n> D := λne Δ,
+  Program Definition ctx_lookup (x : var) : listO D -n> D := λne Δ,
     from_option id (cconst True)%I (Δ !! x).
   Solve Obligations with solve_proper.
 
-  Program Definition interp_unit : listC D -n> D := λne Δ ww,
+  Program Definition interp_unit : listO D -n> D := λne Δ ww,
     (⌜ww.1 = UnitV⌝ ∧ ⌜ww.2 = UnitV⌝)%I.
   Solve Obligations with solve_proper_alt.
-  Program Definition interp_nat : listC D -n> D := λne Δ ww,
+  Program Definition interp_nat : listO D -n> D := λne Δ ww,
     (∃ n : nat, ⌜ww.1 = #nv n⌝ ∧ ⌜ww.2 = #nv n⌝)%I.
   Solve Obligations with solve_proper.
 
-  Program Definition interp_bool : listC D -n> D := λne Δ ww,
+  Program Definition interp_bool : listO D -n> D := λne Δ ww,
     (∃ b : bool, ⌜ww.1 = #♭v b⌝ ∧ ⌜ww.2 = #♭v b⌝)%I.
   Solve Obligations with solve_proper.
 
   Program Definition interp_prod
-      (interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ ww,
+      (interp1 interp2 : listO D -n> D) : listO D -n> D := λne Δ ww,
     (∃ vv1 vv2, ⌜ww = (PairV (vv1.1) (vv2.1), PairV (vv1.2) (vv2.2))⌝ ∧
                 interp1 Δ vv1 ∧ interp2 Δ vv2)%I.
   Solve Obligations with solve_proper.
 
   Program Definition interp_sum
-      (interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ ww,
+      (interp1 interp2 : listO D -n> D) : listO D -n> D := λne Δ ww,
     ((∃ vv, ⌜ww = (InjLV (vv.1), InjLV (vv.2))⌝ ∧ interp1 Δ vv) ∨
      (∃ vv, ⌜ww = (InjRV (vv.1), InjRV (vv.2))⌝ ∧ interp2 Δ vv))%I.
   Solve Obligations with solve_proper.
 
   Program Definition interp_arrow
-          (interp1 interp2 : listC D -n> D) : listC D -n> D :=
+          (interp1 interp2 : listO D -n> D) : listO D -n> D :=
     λne Δ ww,
     (□ ∀ vv, interp1 Δ vv →
              interp_expr
@@ -78,7 +78,7 @@ Section logrel.
   Solve Obligations with solve_proper.
 
   Program Definition interp_forall
-      (interp : listC D -n> D) : listC D -n> D := λne Δ ww,
+      (interp : listO D -n> D) : listO D -n> D := λne Δ ww,
     (□ ∀ τi,
           ⌜∀ ww, Persistent (τi ww)⌝ →
           interp_expr
@@ -86,19 +86,19 @@ Section logrel.
   Solve Obligations with solve_proper.
 
   Program Definition interp_rec1
-      (interp : listC D -n> D) (Δ : listC D) (τi : D) : D := λne ww,
+      (interp : listO D -n> D) (Δ : listO D) (τi : D) : D := λne ww,
     (□ ∃ vv, ⌜ww = (FoldV (vv.1), FoldV (vv.2))⌝ ∧ ▷ interp (τi :: Δ) vv)%I.
   Solve Obligations with solve_proper.
 
   Global Instance interp_rec1_contractive
-    (interp : listC D -n> D) (Δ : listC D) : Contractive (interp_rec1 interp Δ).
+    (interp : listO D -n> D) (Δ : listO D) : Contractive (interp_rec1 interp Δ).
   Proof. solve_contractive. Qed.
 
-  Lemma fixpoint_interp_rec1_eq (interp : listC D -n> D) Δ x :
+  Lemma fixpoint_interp_rec1_eq (interp : listO D -n> D) Δ x :
     fixpoint (interp_rec1 interp Δ) x ≡ interp_rec1 interp Δ (fixpoint (interp_rec1 interp Δ)) x.
   Proof. exact: (fixpoint_unfold (interp_rec1 interp Δ) x). Qed.
 
-  Program Definition interp_rec (interp : listC D -n> D) : listC D -n> D := λne Δ,
+  Program Definition interp_rec (interp : listO D -n> D) : listO D -n> D := λne Δ,
     fixpoint (interp_rec1 interp Δ).
   Next Obligation.
     intros interp n Δ1 Δ2 HΔ; apply fixpoint_ne => τi ww. solve_proper.
@@ -109,12 +109,12 @@ Section logrel.
   Solve Obligations with solve_proper.
 
   Program Definition interp_ref
-      (interp : listC D -n> D) : listC D -n> D := λne Δ ww,
+      (interp : listO D -n> D) : listO D -n> D := λne Δ ww,
     (∃ ll, ⌜ww = (LocV (ll.1), LocV (ll.2))⌝ ∧
            inv (logN .@ ll) (interp_ref_inv ll (interp Δ)))%I.
   Solve Obligations with solve_proper.
 
-  Fixpoint interp (Ï„ : type) : listC D -n> D :=
+  Fixpoint interp (Ï„ : type) : listO D -n> D :=
     match Ï„ return _ with
     | TUnit => interp_unit
     | TNat => interp_nat
@@ -130,7 +130,7 @@ Section logrel.
   Notation "⟦ τ ⟧" := (interp τ).
 
   Definition interp_env (Γ : list type)
-      (Δ : listC D) (vvs : list (val * val)) : iProp Σ :=
+      (Δ : listO D) (vvs : list (val * val)) : iProp Σ :=
     (⌜length Γ = length vvs⌝ ∗ [∗] zip_with (λ τ, ⟦ τ ⟧ Δ) Γ vvs)%I.
   Notation "⟦ Γ ⟧*" := (interp_env Γ).
 
@@ -174,7 +174,7 @@ Section logrel.
     - rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl.
       { by rewrite !lookup_app_l. }
       (* FIXME: Ideally we wouldn't have to do this kinf of surgery. *)
-      change (bi_ofeC (uPredI (iResUR Σ))) with (uPredC (iResUR Σ)).
+      change (bi_ofeO (uPredI (iResUR Σ))) with (uPredO (iResUR Σ)).
       rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia.
     - unfold interp_expr.
       intros ww; simpl; properness; auto. by apply (IHÏ„ (_ :: _)).
@@ -195,11 +195,11 @@ Section logrel.
     - rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl.
       { by rewrite !lookup_app_l. }
       (* FIXME: Ideally we wouldn't have to do this kinf of surgery. *)
-      change (bi_ofeC (uPredI (iResUR Σ))) with (uPredC (iResUR Σ)).
+      change (bi_ofeO (uPredI (iResUR Σ))) with (uPredO (iResUR Σ)).
       rewrite !lookup_app_r; [|lia ..].
       case EQ: (x - length Δ1) => [|n]; simpl.
       { symmetry. asimpl. apply (interp_weaken [] Δ1 Δ2 τ'). }
-      change (bi_ofeC (uPredI (iResUR Σ))) with (uPredC (iResUR Σ)).
+      change (bi_ofeO (uPredI (iResUR Σ))) with (uPredO (iResUR Σ)).
       rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia.
     - unfold interp_expr.
       intros ww; simpl; properness; auto. apply (IHÏ„ (_ :: _)).
diff --git a/theories/logrel/F_mu_ref_conc/logrel_unary.v b/theories/logrel/F_mu_ref_conc/logrel_unary.v
index 53715af0032bb367ffa819e9380ef77ebfd436d9..a1da8812dad1a577651b6270dcb802599fc1593b 100644
--- a/theories/logrel/F_mu_ref_conc/logrel_unary.v
+++ b/theories/logrel/F_mu_ref_conc/logrel_unary.v
@@ -10,53 +10,53 @@ Definition logN : namespace := nroot .@ "logN".
 (** interp : is a unary logical relation. *)
 Section logrel.
   Context `{heapIG Σ}.
-  Notation D := (valC -n> iProp Σ).
+  Notation D := (valO -n> iProp Σ).
   Implicit Types Ï„i : D.
-  Implicit Types Δ : listC D.
-  Implicit Types interp : listC D → D.
+  Implicit Types Δ : listO D.
+  Implicit Types interp : listO D → D.
 
-  Program Definition env_lookup (x : var) : listC D -n> D := λne Δ,
+  Program Definition env_lookup (x : var) : listO D -n> D := λne Δ,
     from_option id (cconst True)%I (Δ !! x).
   Solve Obligations with solve_proper.
 
-  Definition interp_unit : listC D -n> D := λne Δ w, ⌜w = UnitV⌝%I.
-  Definition interp_nat : listC D -n> D := λne Δ w, ⌜∃ n, w = #nv n⌝%I.
-  Definition interp_bool : listC D -n> D := λne Δ w, ⌜∃ n, w = #♭v n⌝%I.
+  Definition interp_unit : listO D -n> D := λne Δ w, ⌜w = UnitV⌝%I.
+  Definition interp_nat : listO D -n> D := λne Δ w, ⌜∃ n, w = #nv n⌝%I.
+  Definition interp_bool : listO D -n> D := λne Δ w, ⌜∃ n, w = #♭v n⌝%I.
 
   Program Definition interp_prod
-      (interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ w,
+      (interp1 interp2 : listO D -n> D) : listO D -n> D := λne Δ w,
     (∃ w1 w2, ⌜w = PairV w1 w2⌝ ∧ interp1 Δ w1 ∧ interp2 Δ w2)%I.
   Solve Obligations with repeat intros ?; simpl; solve_proper.
 
   Program Definition interp_sum
-      (interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ w,
+      (interp1 interp2 : listO D -n> D) : listO D -n> D := λne Δ w,
     ((∃ w1, ⌜w = InjLV w1⌝ ∧ interp1 Δ w1) ∨ (∃ w2, ⌜w = InjRV w2⌝ ∧ interp2 Δ w2))%I.
   Solve Obligations with repeat intros ?; simpl; solve_proper.
 
   Program Definition interp_arrow
-      (interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ w,
+      (interp1 interp2 : listO D -n> D) : listO D -n> D := λne Δ w,
     (□ ∀ v, interp1 Δ v → WP App (of_val w) (of_val v) {{ interp2 Δ }})%I.
   Solve Obligations with repeat intros ?; simpl; solve_proper.
 
   Program Definition interp_forall
-      (interp : listC D -n> D) : listC D -n> D := λne Δ w,
+      (interp : listO D -n> D) : listO D -n> D := λne Δ w,
     (□ ∀ τi : D,
       ⌜∀ v, Persistent (τi v)⌝ → WP TApp (of_val w) {{ interp (τi :: Δ) }})%I.
   Solve Obligations with repeat intros ?; simpl; solve_proper.
 
   Definition interp_rec1
-      (interp : listC D -n> D) (Δ : listC D) (τi : D) : D := λne w,
+      (interp : listO D -n> D) (Δ : listO D) (τi : D) : D := λne w,
     (□ (∃ v, ⌜w = FoldV v⌝ ∧ ▷ interp (τi :: Δ) v))%I.
 
   Global Instance interp_rec1_contractive
-    (interp : listC D -n> D) (Δ : listC D) : Contractive (interp_rec1 interp Δ).
+    (interp : listO D -n> D) (Δ : listO D) : Contractive (interp_rec1 interp Δ).
   Proof. by solve_contractive. Qed.
 
-  Lemma fixpoint_interp_rec1_eq (interp : listC D -n> D) Δ x :
+  Lemma fixpoint_interp_rec1_eq (interp : listO D -n> D) Δ x :
     fixpoint (interp_rec1 interp Δ) x ≡ interp_rec1 interp Δ (fixpoint (interp_rec1 interp Δ)) x.
   Proof. exact: (fixpoint_unfold (interp_rec1 interp Δ) x). Qed.
 
-  Program Definition interp_rec (interp : listC D -n> D) : listC D -n> D := λne Δ,
+  Program Definition interp_rec (interp : listO D -n> D) : listO D -n> D := λne Δ,
     fixpoint (interp_rec1 interp Δ).
   Next Obligation.
     intros interp n Δ1 Δ2 HΔ; apply fixpoint_ne => τi w. solve_proper.
@@ -67,11 +67,11 @@ Section logrel.
   Solve Obligations with solve_proper.
 
   Program Definition interp_ref
-      (interp : listC D -n> D) : listC D -n> D := λne Δ w,
+      (interp : listO D -n> D) : listO D -n> D := λne Δ w,
     (∃ l, ⌜w = LocV l⌝ ∧ inv (logN .@ l) (interp_ref_inv l (interp Δ)))%I.
   Solve Obligations with solve_proper.
 
-  Fixpoint interp (Ï„ : type) : listC D -n> D :=
+  Fixpoint interp (Ï„ : type) : listO D -n> D :=
     match Ï„ return _ with
     | TUnit => interp_unit
     | TNat => interp_nat
@@ -87,11 +87,11 @@ Section logrel.
   Notation "⟦ τ ⟧" := (interp τ).
 
   Definition interp_env (Γ : list type)
-      (Δ : listC D) (vs : list val) : iProp Σ :=
+      (Δ : listO D) (vs : list val) : iProp Σ :=
     (⌜length Γ = length vs⌝ ∗ [∗] zip_with (λ τ, ⟦ τ ⟧ Δ) Γ vs)%I.
   Notation "⟦ Γ ⟧*" := (interp_env Γ).
 
-  Definition interp_expr (τ : type) (Δ : listC D) (e : expr) : iProp Σ :=
+  Definition interp_expr (τ : type) (Δ : listO D) (e : expr) : iProp Σ :=
     WP e {{ ⟦ τ ⟧ Δ }}%I.
 
   Class env_Persistent Δ :=
@@ -133,7 +133,7 @@ Section logrel.
     - rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl.
       { by rewrite !lookup_app_l. }
       (* FIXME: Ideally we wouldn't have to do this kinf of surgery. *)
-      change (bi_ofeC (uPredI (iResUR Σ))) with (uPredC (iResUR Σ)).
+      change (bi_ofeO (uPredI (iResUR Σ))) with (uPredO (iResUR Σ)).
       rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia.
     - intros w; simpl; properness; auto. apply (IHÏ„ (_ :: _)).
     - intros w; simpl; properness; auto. by apply IHÏ„.
@@ -152,11 +152,11 @@ Section logrel.
     - rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl.
       { by rewrite !lookup_app_l. }
       (* FIXME: Ideally we wouldn't have to do this kinf of surgery. *)
-      change (bi_ofeC (uPredI (iResUR Σ))) with (uPredC (iResUR Σ)).
+      change (bi_ofeO (uPredI (iResUR Σ))) with (uPredO (iResUR Σ)).
       rewrite !lookup_app_r; [|lia ..].
       case EQ: (x - length Δ1) => [|n]; simpl.
       { symmetry. asimpl. apply (interp_weaken [] Δ1 Δ2 τ'). }
-      change (bi_ofeC (uPredI (iResUR Σ))) with (uPredC (iResUR Σ)).
+      change (bi_ofeO (uPredI (iResUR Σ))) with (uPredO (iResUR Σ)).
       rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia.
     - intros w; simpl; properness; auto. apply (IHÏ„ (_ :: _)).
     - intros w; simpl; properness; auto. by apply IHÏ„.
diff --git a/theories/logrel/F_mu_ref_conc/rules_binary.v b/theories/logrel/F_mu_ref_conc/rules_binary.v
index 7c2449c084ebff96740364625142ac61b0712831..1d8f47e9aff9b58c1a54ed6e50f175d6f27ceb5f 100644
--- a/theories/logrel/F_mu_ref_conc/rules_binary.v
+++ b/theories/logrel/F_mu_ref_conc/rules_binary.v
@@ -8,7 +8,7 @@ Import uPred.
 Definition specN := nroot .@ "spec".
 
 (** The CMRA for the heap of the specification. *)
-Definition tpoolUR : ucmraT := gmapUR nat (exclR exprC).
+Definition tpoolUR : ucmraT := gmapUR nat (exclR exprO).
 Definition cfgUR := prodUR tpoolUR (gen_heapUR loc val).
 
 Fixpoint to_tpool_go (i : nat) (tp : list expr) : tpoolUR :=
@@ -107,7 +107,7 @@ Section conversions.
     - by rewrite lookup_insert tpool_lookup lookup_app_r // Nat.sub_diag.
     - rewrite lookup_insert_ne; last lia.
       rewrite !tpool_lookup ?lookup_ge_None_2 ?app_length //=;
-         change (ofe_car exprC) with expr; lia.
+         change (ofe_car exprO) with expr; lia.
   Qed.
 
   Lemma tpool_singleton_included tp j e :
diff --git a/theories/logrel/prelude/base.v b/theories/logrel/prelude/base.v
index ce6f8bef757c932a8b2b90e8d214edb7c1d64c99..1007bee3497f775f1a6d96bce4a7d4981f53214b 100644
--- a/theories/logrel/prelude/base.v
+++ b/theories/logrel/prelude/base.v
@@ -5,7 +5,7 @@ From iris.base_logic Require Import invariants.
 From Autosubst Require Export Autosubst.
 Import uPred.
 
-Canonical Structure varC := leibnizC var.
+Canonical Structure varO := leibnizO var.
 
 Section Autosubst_Lemmas.
   Context {term : Type} {Ids_term : Ids term}
diff --git a/theories/logrel_heaplang/ltyping.v b/theories/logrel_heaplang/ltyping.v
index ed3fb03443609dcac13de08b3a3ce2fb04e412a1..4e35302fa1ce3f81a20772cf66a250bedcd0e10f 100644
--- a/theories/logrel_heaplang/ltyping.v
+++ b/theories/logrel_heaplang/ltyping.v
@@ -20,11 +20,11 @@ Section lty_ofe.
   Instance lty_equiv : Equiv (lty Σ) := λ A B, ∀ w, A w ≡ B w.
   Instance lty_dist : Dist (lty Σ) := λ n A B, ∀ w, A w ≡{n}≡ B w.
   Lemma lty_ofe_mixin : OfeMixin (lty Σ).
-  Proof. by apply (iso_ofe_mixin (lty_car : _ → val -c> _)). Qed.
+  Proof. by apply (iso_ofe_mixin (lty_car : _ → val -d> _)). Qed.
   Canonical Structure ltyC := OfeT (lty Σ) lty_ofe_mixin.
   Global Instance lty_cofe : Cofe ltyC.
   Proof.
-    apply (iso_cofe_subtype' (λ A : val -c> iProp Σ, ∀ w, Persistent (A w))
+    apply (iso_cofe_subtype' (λ A : val -d> iProp Σ, ∀ w, Persistent (A w))
       (@Lty _) lty_car)=> //.
     - apply _.
     - apply limit_preserving_forall=> w.
diff --git a/theories/spanning_tree/mon.v b/theories/spanning_tree/mon.v
index 9e14e57adf867ea9e3c72762ff72ae3b9e3f5601..3173b076fb17303a4c14d720d5dcdc3ed3591b85 100644
--- a/theories/spanning_tree/mon.v
+++ b/theories/spanning_tree/mon.v
@@ -11,11 +11,11 @@ From stdpp Require Import gmap mapset.
 From iris_examples.spanning_tree Require Import graph.
 
 (* children cofe *)
-Canonical Structure chlC := leibnizC (option loc * option loc).
+Canonical Structure chlO := leibnizO (option loc * option loc).
 (* The graph monoid. *)
 Definition graphN : namespace := nroot .@ "SPT_graph".
 Definition graphUR : ucmraT :=
-  optionUR (prodR fracR (gmapR loc (exclR chlC))).
+  optionUR (prodR fracR (gmapR loc (exclR chlO))).
 (* The monoid for talking about which nodes are marked.
 These markings are duplicatable. *)
 Definition markingUR : ucmraT := gsetUR loc.
@@ -67,9 +67,9 @@ Section marking_definitions.
 End marking_definitions.
 
 (* The monoid representing graphs *)
-Definition Gmon := gmapR loc (exclR chlC).
+Definition Gmon := gmapR loc (exclR chlO).
 
-Definition excl_chlC_chl (ch : exclR chlC) : option (option loc * option loc) :=
+Definition excl_chlC_chl (ch : exclR chlO) : option (option loc * option loc) :=
   match ch with
   | Excl w => Some w
   | Excl_Bot => None
@@ -533,7 +533,7 @@ Lemma graph_op_path' (G G' : Gmon) x z p :
   ✓ (G ⋅ G') → x ∈ dom (gset _) G' → valid_path (Gmon_graph G) z x p → False.
 Proof. rewrite comm; apply graph_op_path. Qed.
 
-Lemma in_dom_singleton (x : loc) (w : chlC) :
+Lemma in_dom_singleton (x : loc) (w : chlO) :
   x ∈ dom (gset loc) (x [↦] w : gmap loc _).
 Proof. by rewrite dom_singleton elem_of_singleton. Qed.
 
diff --git a/theories/spanning_tree/spanning.v b/theories/spanning_tree/spanning.v
index 6afd1516514cffeca605b39dce8160cd965a9b62..661cc5911e1394066dec96ba23a55dd029b7f697 100644
--- a/theories/spanning_tree/spanning.v
+++ b/theories/spanning_tree/spanning.v
@@ -244,7 +244,7 @@ Section Helpers.
     - intros x; rewrite elem_of_union; intuition.
     - intros x y; rewrite elem_of_union; intuition eauto.
   Qed.
-  Lemma front_singleton (g : graph loc) (t : gset loc) l (w : chlC) u1 u2 :
+  Lemma front_singleton (g : graph loc) (t : gset loc) l (w : chlO) u1 u2 :
     g !! l = Some (u1, u2) →
     match u1 with |Some l1 => l1 ∈ t | None => True end →
     match u2 with |Some l2 => l2 ∈ t | None => True end →
@@ -259,8 +259,8 @@ Section Helpers.
   Lemma empty_graph_divide q :
     own_graph q ∅ ⊢ own_graph (q / 2) ∅ ∗ own_graph (q / 2) ∅.
   Proof.
-    setoid_replace (∅ : gmapR loc (exclR chlC)) with
-    (∅ ⋅ ∅ : gmapR loc (exclR chlC)) at 1 by (by rewrite ucmra_unit_left_id).
+    setoid_replace (∅ : gmapR loc (exclR chlO)) with
+    (∅ ⋅ ∅ : gmapR loc (exclR chlO)) at 1 by (by rewrite ucmra_unit_left_id).
     by rewrite graph_divide.
   Qed.