diff --git a/theories/algebra/coPset.v b/theories/algebra/coPset.v
index e3e717a6ec1c40ec205ffea1d1dbb4bccd5c025c..326c0251dd2f0ac1123038d67b4ec2378e3695e9 100644
--- a/theories/algebra/coPset.v
+++ b/theories/algebra/coPset.v
@@ -67,7 +67,7 @@ Inductive coPset_disj :=
 
 Section coPset_disj.
   Arguments op _ _ !_ !_ /.
-  Canonical Structure coPset_disjC := leibnizO coPset_disj.
+  Canonical Structure coPset_disjO := leibnizO coPset_disj.
 
   Instance coPset_disj_valid : Valid coPset_disj := λ X,
     match X with CoPset _ => True | CoPsetBot => False end.
diff --git a/theories/algebra/deprecated.v b/theories/algebra/deprecated.v
index 5f9732894073ab1b9c373c7dcce59feb6a9ae3ec..d91ece95affa891911e3ed583502710dbc9f953d 100644
--- a/theories/algebra/deprecated.v
+++ b/theories/algebra/deprecated.v
@@ -29,7 +29,7 @@ Implicit Types x y : dec_agree A.
 
 Instance dec_agree_valid : Valid (dec_agree A) := λ x,
   if x is DecAgree _ then True else False.
-Canonical Structure dec_agreeC : ofeT := leibnizO (dec_agree A).
+Canonical Structure dec_agreeO : ofeT := leibnizO (dec_agree A).
 
 Instance dec_agree_op : Op (dec_agree A) := λ x y,
   match x, y with
@@ -74,6 +74,6 @@ Proof.
 Qed.
 End dec_agree.
 
-Arguments dec_agreeC : clear implicits.
+Arguments dec_agreeO : clear implicits.
 Arguments dec_agreeR _ {_}.
 End dec_agree.
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 61dc5698696761f3f7da82d7d198b1a0e2a89093..1974baea5df46fcba66a2dd52782428027aee520 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -1107,7 +1107,7 @@ Qed.
 (** We make [discrete_fun] a definition so that we can register it as a
 canonical structure. Note that non-dependent functions over a discrete domain,
 [discrete_fun (λ _, A) B] (or [A -d> B] following the notation we introduce
-below) are isomorphic to [leibnizC A -n> B]. In other words, since the domain
+below) are isomorphic to [leibnizO A -n> B]. In other words, since the domain
 is discrete, we get non-expansiveness for free. *)
 Definition discrete_fun {A} (B : A → ofeT) := ∀ x : A, B x.
 
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index 0efa3739a8a3ade1804870814ccfae15b6943bd4..309940e3b067c6766ff234dafb0645acde1cbb82 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -60,7 +60,7 @@ this RA would be quite inconvenient to deal with. *)
 Definition gen_heapUR (L V : Type) `{Countable L} : ucmraT :=
   gmapUR L (prodR fracR (agreeR (leibnizO V))).
 Definition gen_metaUR (L : Type) `{Countable L} : ucmraT :=
-  gmapUR L (agreeR gnameC).
+  gmapUR L (agreeR gnameO).
 
 Definition to_gen_heap {L V} `{Countable L} : gmap L V → gen_heapUR L V :=
   fmap (λ v, (1%Qp, to_agree (v : leibnizO V))).
diff --git a/theories/base_logic/lib/iprop.v b/theories/base_logic/lib/iprop.v
index 0062aa9cd71de7e1ffbfcb5f7462272423bd786d..809bfe6409449898a8fd393ec71652509825f76f 100644
--- a/theories/base_logic/lib/iprop.v
+++ b/theories/base_logic/lib/iprop.v
@@ -45,7 +45,7 @@ Definition gFunctors_lookup (Σ : gFunctors) : gid Σ → gFunctor := projT2 Σ.
 Coercion gFunctors_lookup : gFunctors >-> Funclass.
 
 Definition gname := positive.
-Canonical Structure gnameC := leibnizO gname.
+Canonical Structure gnameO := leibnizO gname.
 
 (** The resources functor [iResF Σ A := ∀ i : gid, gname -fin-> (Σ i) A]. *)
 Definition iResF (Σ : gFunctors) : urFunctor :=