From 782f2970d4ad152777771d46b61defb352e6c7d1 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 18 Jun 2019 20:25:57 +0200
Subject: [PATCH] =?UTF-8?q?Some=20forgotten=20C=E2=86=92O=20renames.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/algebra/coPset.v          | 2 +-
 theories/algebra/deprecated.v      | 4 ++--
 theories/algebra/ofe.v             | 2 +-
 theories/base_logic/lib/gen_heap.v | 2 +-
 theories/base_logic/lib/iprop.v    | 2 +-
 5 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/theories/algebra/coPset.v b/theories/algebra/coPset.v
index e3e717a6e..326c0251d 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 5f9732894..d91ece95a 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 61dc56986..1974baea5 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 0efa3739a..309940e3b 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 0062aa9cd..809bfe640 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 :=
-- 
GitLab