Merge branch 'robbert/ofe_rename' into 'master'

Replace `C`s with `O`s since we use OFEs instead of COFEs.

Closes #118

See merge request iris/iris!263

StyleGuide.md

@@ -36,8 +36,8 @@ is used by clients.
 
 ### small letters
 
-* a : A = cmraT or cofeT
-* b : B = cmraT or cofeT
+* a : A = cmraT or ofeT
+* b : B = cmraT or ofeT
 * c
 * d
 * e : expr = expressions
@@ -67,8 +67,8 @@ is used by clients.
 
 ### capital letters
 
-* A : Type, cmraT or cofeT
-* B : Type, cmraT or cofeT
+* A : Type, cmraT or ofeT
+* B : Type, cmraT or ofeT
 * C
 * D   
 * E : coPset = Viewshift masks
@@ -110,9 +110,9 @@ is used by clients.
 
 ### Suffixes
 
-* C: OFEs
+* O: OFEs
 * R: cameras
 * UR: unital cameras or resources algebras
-* F: functors (can be combined with all of the above, e.g. CF is an OFE functor)
+* F: functors (can be combined with all of the above, e.g. OF is an OFE functor)
 * G: global camera functor management
 * T: canonical structurs for algebraic classes (for example ofeT for OFEs, cmraT for cameras)

tests/ipm_paper.v

@@ -132,7 +132,7 @@ Section M.
   Arguments op _ _ !_ !_/.
   Arguments core _ _ !_/.
 
-  Canonical Structure M_C : ofeT := leibnizC M.
+  Canonical Structure M_O : ofeT := leibnizO M.
 
   Instance M_valid : Valid M := λ x, x ≠ Bot.
   Instance M_op : Op M := λ x y,

tests/one_shot.v

@@ -21,7 +21,7 @@ Definition one_shot_example : val := λ: <>,
        end
     end)).
 
-Definition one_shotR := csumR (exclR unitC) (agreeR ZC).
+Definition one_shotR := csumR (exclR unitO) (agreeR ZO).
 Definition Pending : one_shotR := Cinl (Excl ()).
 Definition Shot (n : Z) : one_shotR := Cinr (to_agree n).
 

theories/algebra/agree.v

@@ -75,7 +75,7 @@ Proof.
         destruct (H1' b) as (c&?&?); eauto. by exists c; split; last etrans.
   - intros n x y [??]; split; naive_solver eauto using dist_S.
 Qed.
-Canonical Structure agreeC := OfeT (agree A) agree_ofe_mixin.
+Canonical Structure agreeO := OfeT (agree A) agree_ofe_mixin.
 
 (* CMRA *)
 (* agree_validN is carefully written such that, when applied to a singleton, it
@@ -251,7 +251,7 @@ Proof. uPred.unseal. split=> n y _. exact: to_agree_uninjN. Qed.
 End agree.
 
 Instance: Params (@to_agree) 1 := {}.
-Arguments agreeC : clear implicits.
+Arguments agreeO : clear implicits.
 Arguments agreeR : clear implicits.
 
 Program Definition agree_map {A B} (f : A → B) (x : agree A) : agree B :=
@@ -297,33 +297,33 @@ Section agree_map.
   Qed.
 End agree_map.
 
-Definition agreeC_map {A B} (f : A -n> B) : agreeC A -n> agreeC B :=
-  CofeMor (agree_map f : agreeC A → agreeC B).
-Instance agreeC_map_ne A B : NonExpansive (@agreeC_map A B).
+Definition agreeO_map {A B} (f : A -n> B) : agreeO A -n> agreeO B :=
+  OfeMor (agree_map f : agreeO A → agreeO B).
+Instance agreeO_map_ne A B : NonExpansive (@agreeO_map A B).
 Proof.
   intros n f g Hfg x; split=> b /=;
     setoid_rewrite elem_of_list_fmap; naive_solver.
 Qed.
 
-Program Definition agreeRF (F : cFunctor) : rFunctor := {|
-  rFunctor_car A _ B _ := agreeR (cFunctor_car F A B);
-  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := agreeC_map (cFunctor_map F fg)
+Program Definition agreeRF (F : oFunctor) : rFunctor := {|
+  rFunctor_car A _ B _ := agreeR (oFunctor_car F A B);
+  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := agreeO_map (oFunctor_map F fg)
 |}.
 Next Obligation.
-  intros ? A1 ? A2 ? B1 ? B2 ? n ???; simpl. by apply agreeC_map_ne, cFunctor_ne.
+  intros ? A1 ? A2 ? B1 ? B2 ? n ???; simpl. by apply agreeO_map_ne, oFunctor_ne.
 Qed.
 Next Obligation.
   intros F A ? B ? x; simpl. rewrite -{2}(agree_map_id x).
-  apply (agree_map_ext _)=>y. by rewrite cFunctor_id.
+  apply (agree_map_ext _)=>y. by rewrite oFunctor_id.
 Qed.
 Next Obligation.
   intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl. rewrite -agree_map_compose.
-  apply (agree_map_ext _)=>y; apply cFunctor_compose.
+  apply (agree_map_ext _)=>y; apply oFunctor_compose.
 Qed.
 
 Instance agreeRF_contractive F :
-  cFunctorContractive F → rFunctorContractive (agreeRF F).
+  oFunctorContractive F → rFunctorContractive (agreeRF F).
 Proof.
   intros ? A1 ? A2 ? B1 ? B2 ? n ???; simpl.
-  by apply agreeC_map_ne, cFunctor_contractive.
+  by apply agreeO_map_ne, oFunctor_contractive.
 Qed.

theories/algebra/auth.v

@@ -62,16 +62,16 @@ Proof. by destruct 1. Qed.
 
 Definition auth_ofe_mixin : OfeMixin (auth A).
 Proof. by apply (iso_ofe_mixin (λ x, (auth_auth_proj x, auth_frag_proj x))). Qed.
-Canonical Structure authC := OfeT (auth A) auth_ofe_mixin.
+Canonical Structure authO := OfeT (auth A) auth_ofe_mixin.
 
 Global Instance Auth_discrete a b :
   Discrete a → Discrete b → Discrete (Auth a b).
 Proof. by intros ?? [??] [??]; split; apply: discrete. Qed.
-Global Instance auth_ofe_discrete : OfeDiscrete A → OfeDiscrete authC.
+Global Instance auth_ofe_discrete : OfeDiscrete A → OfeDiscrete authO.
 Proof. intros ? [??]; apply _. Qed.
 End ofe.
 
-Arguments authC : clear implicits.
+Arguments authO : clear implicits.
 
 (* Camera *)
 Section cmra.
@@ -430,18 +430,18 @@ Proof.
   - intros [[[??]|]?] [[[??]|]?]; try apply Auth_proper=>//=; try by rewrite cmra_morphism_op.
     by rewrite -Some_op pair_op cmra_morphism_op.
 Qed.
-Definition authC_map {A B} (f : A -n> B) : authC A -n> authC B :=
-  CofeMor (auth_map f).
-Lemma authC_map_ne A B : NonExpansive (@authC_map A B).
+Definition authO_map {A B} (f : A -n> B) : authO A -n> authO B :=
+  OfeMor (auth_map f).
+Lemma authO_map_ne A B : NonExpansive (@authO_map A B).
 Proof. intros n f f' Hf [[[]|] ]; repeat constructor; try naive_solver;
-  apply agreeC_map_ne; auto. Qed.
+  apply agreeO_map_ne; auto. Qed.
 
 Program Definition authRF (F : urFunctor) : rFunctor := {|
   rFunctor_car A _ B _ := authR (urFunctor_car F A B);
-  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := authC_map (urFunctor_map F fg)
+  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := authO_map (urFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authC_map_ne, urFunctor_ne.
+  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authO_map_ne, urFunctor_ne.
 Qed.
 Next Obligation.
   intros F A ? B ? x. rewrite /= -{2}(auth_map_id x).
@@ -455,15 +455,15 @@ Qed.
 Instance authRF_contractive F :
   urFunctorContractive F → rFunctorContractive (authRF F).
 Proof.
-  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authC_map_ne, urFunctor_contractive.
+  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authO_map_ne, urFunctor_contractive.
 Qed.
 
 Program Definition authURF (F : urFunctor) : urFunctor := {|
   urFunctor_car A _ B _ := authUR (urFunctor_car F A B);
-  urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := authC_map (urFunctor_map F fg)
+  urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := authO_map (urFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authC_map_ne, urFunctor_ne.
+  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authO_map_ne, urFunctor_ne.
 Qed.
 Next Obligation.
   intros F A ? B ? x. rewrite /= -{2}(auth_map_id x).
@@ -477,5 +477,5 @@ Qed.
 Instance authURF_contractive F :
   urFunctorContractive F → urFunctorContractive (authURF F).
 Proof.
-  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authC_map_ne, urFunctor_contractive.
+  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authO_map_ne, urFunctor_contractive.
 Qed.

theories/algebra/coPset.v

@@ -9,7 +9,7 @@ generalize the construction without breaking canonical structures. *)
 Section coPset.
   Implicit Types X Y : coPset.
 
-  Canonical Structure coPsetC := discreteC coPset.
+  Canonical Structure coPsetO := discreteO coPset.
 
   Instance coPset_valid : Valid coPset := λ _, True.
   Instance coPset_unit : Unit coPset := (∅ : coPset).
@@ -67,7 +67,7 @@ Inductive coPset_disj :=
 
 Section coPset_disj.
   Arguments op _ _ !_ !_ /.
-  Canonical Structure coPset_disjC := leibnizC coPset_disj.
+  Canonical Structure coPset_disjC := leibnizO coPset_disj.
 
   Instance coPset_disj_valid : Valid coPset_disj := λ X,
     match X with CoPset _ => True | CoPsetBot => False end.

theories/algebra/cofe_solver.v

 From iris.algebra Require Export ofe.
 Set Default Proof Using "Type".
 
-Record solution (F : cFunctor) := Solution {
+Record solution (F : oFunctor) := Solution {
   solution_car :> ofeT;
   solution_cofe : Cofe solution_car;
   solution_unfold : solution_car -n> F solution_car _;
@@ -14,23 +14,23 @@ Arguments solution_fold {_} _.
 Existing Instance solution_cofe.
 
 Module solver. Section solver.
-Context (F : cFunctor) `{Fcontr : cFunctorContractive F}.
+Context (F : oFunctor) `{Fcontr : oFunctorContractive F}.
 Context `{Fcofe : ∀ (T : ofeT) `{!Cofe T}, Cofe (F T _)}.
-Context `{Finh : Inhabited (F unitC _)}.
-Notation map := (cFunctor_map F).
+Context `{Finh : Inhabited (F unitO _)}.
+Notation map := (oFunctor_map F).
 
 Fixpoint A' (k : nat) : { C : ofeT & Cofe C } :=
   match k with
-  | 0 => existT (P:=Cofe) unitC _
+  | 0 => existT (P:=Cofe) unitO _
   | S k => existT (P:=Cofe) (F (projT1 (A' k)) (projT2 (A' k))) _
   end.
 Notation A k := (projT1 (A' k)).
 Local Instance A_cofe k : Cofe (A k) := projT2 (A' k).
 
 Fixpoint f (k : nat) : A k -n> A (S k) :=
-  match k with 0 => CofeMor (λ _, inhabitant) | S k => map (g k,f k) end
+  match k with 0 => OfeMor (λ _, inhabitant) | S k => map (g k,f k) end
 with g (k : nat) : A (S k) -n> A k :=
-  match k with 0 => CofeMor (λ _, ()) | S k => map (f k,g k) end.
+  match k with 0 => OfeMor (λ _, ()) | S k => map (f k,g k) end.
 Definition f_S k (x : A (S k)) : f (S k) x = map (g k,f k) x := eq_refl.
 Definition g_S k (x : A (S (S k))) : g (S k) x = map (f k,g k) x := eq_refl.
 Arguments f : simpl never.
@@ -39,14 +39,14 @@ Arguments g : simpl never.
 Lemma gf {k} (x : A k) : g k (f k x) ≡ x.
 Proof using Fcontr.
   induction k as [|k IH]; simpl in *; [by destruct x|].
-  rewrite -cFunctor_compose -{2}[x]cFunctor_id. by apply (contractive_proper map).
+  rewrite -oFunctor_compose -{2}[x]oFunctor_id. by apply (contractive_proper map).
 Qed.
 Lemma fg {k} (x : A (S (S k))) : f (S k) (g (S k) x) ≡{k}≡ x.
 Proof using Fcontr.
   induction k as [|k IH]; simpl.
-  - rewrite f_S g_S -{2}[x]cFunctor_id -cFunctor_compose.
+  - rewrite f_S g_S -{2}[x]oFunctor_id -oFunctor_compose.
     apply (contractive_0 map).
-  - rewrite f_S g_S -{2}[x]cFunctor_id -cFunctor_compose.
+  - rewrite f_S g_S -{2}[x]oFunctor_id -oFunctor_compose.
     by apply (contractive_S map).
 Qed.
 
@@ -104,7 +104,7 @@ Proof. by induction i as [|i IH]; simpl; [done|rewrite g_tower IH]. Qed.
 
 Instance tower_car_ne k : NonExpansive (λ X, tower_car X k).
 Proof. by intros X Y HX. Qed.
-Definition project (k : nat) : T -n> A k := CofeMor (λ X : T, tower_car X k).
+Definition project (k : nat) : T -n> A k := OfeMor (λ X : T, tower_car X k).
 
 Definition coerce {i j} (H : i = j) : A i -n> A j :=
   eq_rect _ (λ i', A i -n> A i') cid _ H.
@@ -158,7 +158,7 @@ Next Obligation. intros k x i. apply g_embed_coerce. Qed.
 Instance: Params (@embed) 1 := {}.
 Instance embed_ne k : NonExpansive (embed k).
 Proof. by intros n x y Hxy i; rewrite /= Hxy. Qed.
-Definition embed' (k : nat) : A k -n> T := CofeMor (embed k).
+Definition embed' (k : nat) : A k -n> T := OfeMor (embed k).
 Lemma embed_f k (x : A k) : embed (S k) (f k x) ≡ embed k x.
 Proof.
   rewrite equiv_dist=> n i; rewrite /embed /= /embed_coerce.
@@ -188,7 +188,7 @@ Next Obligation.
   assert (∃ k, i = k + n) as [k ?] by (exists (i - n); lia); subst; clear Hi.
   induction k as [|k IH]; simpl; first done.
   rewrite -IH -(dist_le _ _ _ _ (f_tower (k + n) _)); last lia.
-  rewrite f_S -cFunctor_compose.
+  rewrite f_S -oFunctor_compose.
   by apply (contractive_ne map); split=> Y /=; rewrite ?g_tower ?embed_f.
 Qed.
 Definition unfold (X : T) : F T _ := compl (unfold_chain X).
@@ -202,7 +202,7 @@ Program Definition fold (X : F T _) : T :=
   {| tower_car n := g n (map (embed' n,project n) X) |}.
 Next Obligation.
   intros X k. apply (_ : Proper ((≡) ==> (≡)) (g k)).
-  rewrite g_S -cFunctor_compose.
+  rewrite g_S -oFunctor_compose.
   apply (contractive_proper map); split=> Y; [apply embed_f|apply g_tower].
 Qed.
 Instance fold_ne : NonExpansive fold.
@@ -210,14 +210,14 @@ Proof. by intros n X Y HXY k; rewrite /fold /= HXY. Qed.
 
 Theorem result : solution F.
 Proof using Type*.
-  apply (Solution F T _ (CofeMor unfold) (CofeMor fold)).
+  apply (Solution F T _ (OfeMor unfold) (OfeMor fold)).
   - move=> X /=. rewrite equiv_dist=> n k; rewrite /unfold /fold /=.
     rewrite -g_tower -(gg_tower _ n); apply (_ : Proper (_ ==> _) (g _)).
     trans (map (ff n, gg n) (X (S (n + k)))).
     { rewrite /unfold (conv_compl n (unfold_chain X)).
       rewrite -(chain_cauchy (unfold_chain X) n (S (n + k))) /=; last lia.
       rewrite -(dist_le _ _ _ _ (f_tower (n + k) _)); last lia.
-      rewrite f_S -!cFunctor_compose; apply (contractive_ne map); split=> Y.
+      rewrite f_S -!oFunctor_compose; apply (contractive_ne map); split=> Y.
       + rewrite /embed' /= /embed_coerce.
         destruct (le_lt_dec _ _); simpl; [exfalso; lia|].
         by rewrite (ff_ff _ (eq_refl (S n + (0 + k)))) /= gf.
@@ -227,14 +227,14 @@ Proof using Type*.
     assert (∀ i k (x : A (S i + k)) (H : S i + k = i + S k),
       map (ff i, gg i) x ≡ gg i (coerce H x)) as map_ff_gg.
     { intros i; induction i as [|i IH]; intros k' x H; simpl.
-      { by rewrite coerce_id cFunctor_id. }
-      rewrite cFunctor_compose g_coerce; apply IH. }
+      { by rewrite coerce_id oFunctor_id. }
+      rewrite oFunctor_compose g_coerce; apply IH. }
     assert (H: S n + k = n + S k) by lia.
     rewrite (map_ff_gg _ _ _ H).
     apply (_ : Proper (_ ==> _) (gg _)); by destruct H.
   - intros X; rewrite equiv_dist=> n /=.
     rewrite /unfold /= (conv_compl' n (unfold_chain (fold X))) /=.
-    rewrite g_S -!cFunctor_compose -{2}[X]cFunctor_id.
+    rewrite g_S -!oFunctor_compose -{2}[X]oFunctor_id.
     apply (contractive_ne map); split => Y /=.
     + rewrite f_tower. apply dist_S. by rewrite embed_tower.
     + etrans; [apply embed_ne, equiv_dist, g_tower|apply embed_tower].

theories/algebra/csum.v

@@ -73,21 +73,21 @@ Proof.
     + destruct 1; inversion_clear 1; constructor; etrans; eauto.
   - by inversion_clear 1; constructor; apply dist_S.
 Qed.
-Canonical Structure csumC : ofeT := OfeT (csum A B) csum_ofe_mixin.
+Canonical Structure csumO : ofeT := OfeT (csum A B) csum_ofe_mixin.
 
-Program Definition csum_chain_l (c : chain csumC) (a : A) : chain A :=
+Program Definition csum_chain_l (c : chain csumO) (a : A) : chain A :=
   {| chain_car n := match c n return _ with Cinl a' => a' | _ => a end |}.
 Next Obligation. intros c a n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
-Program Definition csum_chain_r (c : chain csumC) (b : B) : chain B :=
+Program Definition csum_chain_r (c : chain csumO) (b : B) : chain B :=
   {| chain_car n := match c n return _ with Cinr b' => b' | _ => b end |}.
 Next Obligation. intros c b n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
-Definition csum_compl `{Cofe A, Cofe B} : Compl csumC := λ c,
+Definition csum_compl `{Cofe A, Cofe B} : Compl csumO := λ c,
   match c 0 with
   | Cinl a => Cinl (compl (csum_chain_l c a))
   | Cinr b => Cinr (compl (csum_chain_r c b))
   | CsumBot => CsumBot
   end.
-Global Program Instance csum_cofe `{Cofe A, Cofe B} : Cofe csumC :=
+Global Program Instance csum_cofe `{Cofe A, Cofe B} : Cofe csumO :=
   {| compl := csum_compl |}.
 Next Obligation.
   intros ?? n c; rewrite /compl /csum_compl.
@@ -97,10 +97,10 @@ Next Obligation.
 Qed.
 
 Global Instance csum_ofe_discrete :
-  OfeDiscrete A → OfeDiscrete B → OfeDiscrete csumC.
+  OfeDiscrete A → OfeDiscrete B → OfeDiscrete csumO.
 Proof. by inversion_clear 3; constructor; apply (discrete _). Qed.
 Global Instance csum_leibniz :
-  LeibnizEquiv A → LeibnizEquiv B → LeibnizEquiv csumC.
+  LeibnizEquiv A → LeibnizEquiv B → LeibnizEquiv csumO.
 Proof. by destruct 3; f_equal; apply leibniz_equiv. Qed.
 
 Global Instance Cinl_discrete a : Discrete a → Discrete (Cinl a).
@@ -109,7 +109,7 @@ Global Instance Cinr_discrete b : Discrete b → Discrete (Cinr b).
 Proof. by inversion_clear 2; constructor; apply (discrete _). Qed.
 End cofe.
 
-Arguments csumC : clear implicits.
+Arguments csumO : clear implicits.
 
 (* Functor on COFEs *)
 Definition csum_map {A A' B B'} (fA : A → A') (fB : B → B')
@@ -134,11 +134,11 @@ Instance csum_map_cmra_ne {A A' B B' : ofeT} n :
   Proper ((dist n ==> dist n) ==> (dist n ==> dist n) ==> dist n ==> dist n)
          (@csum_map A A' B B').
 Proof. intros f f' Hf g g' Hg []; destruct 1; constructor; by apply Hf || apply Hg. Qed.
-Definition csumC_map {A A' B B'} (f : A -n> A') (g : B -n> B') :
-  csumC A B -n> csumC A' B' :=
-  CofeMor (csum_map f g).
-Instance csumC_map_ne A A' B B' :
-  NonExpansive2 (@csumC_map A A' B B').
+Definition csumO_map {A A' B B'} (f : A -n> A') (g : B -n> B') :
+  csumO A B -n> csumO A' B' :=
+  OfeMor (csum_map f g).
+Instance csumO_map_ne A A' B B' :
+  NonExpansive2 (@csumO_map A A' B B').
 Proof. by intros n f f' Hf g g' Hg []; constructor. Qed.
 
 Section cmra.
@@ -368,10 +368,10 @@ Qed.
 
 Program Definition csumRF (Fa Fb : rFunctor) : rFunctor := {|
   rFunctor_car A _ B _ := csumR (rFunctor_car Fa A B) (rFunctor_car Fb A B);
-  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := csumC_map (rFunctor_map Fa fg) (rFunctor_map Fb fg)
+  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := csumO_map (rFunctor_map Fa fg) (rFunctor_map Fb fg)
 |}.
 Next Obligation.
-  by intros Fa Fb A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply csumC_map_ne; try apply rFunctor_ne.
+  by intros Fa Fb A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply csumO_map_ne; try apply rFunctor_ne.
 Qed.
 Next Obligation.
   intros Fa Fb A ? B ? x. rewrite /= -{2}(csum_map_id x).
@@ -387,5 +387,5 @@ Instance csumRF_contractive Fa Fb :
   rFunctorContractive (csumRF Fa Fb).
 Proof.
   intros ?? A1 ? A2 ? B1 ? B2 ? n f g Hfg.
-  by apply csumC_map_ne; try apply rFunctor_contractive.
+  by apply csumO_map_ne; try apply rFunctor_contractive.
 Qed.

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 := leibnizC (dec_agree A).
+Canonical Structure dec_agreeC : ofeT := leibnizO (dec_agree A).
 
 Instance dec_agree_op : Op (dec_agree A) := λ x y,
   match x, y with

theories/algebra/dra.v

@@ -118,7 +118,7 @@ Proof.
   - intros [x px ?] [y py ?] [z pz ?] [? Hxy] [? Hyz]; simpl in *.
     split; [|intros; trans y]; tauto.
 Qed.
-Canonical Structure validityC : ofeT := discreteC (validity A).
+Canonical Structure validityO : ofeT := discreteO (validity A).
 
 Instance dra_valid_proper' : Proper ((≡) ==> iff) (valid : A → Prop).
 Proof. by split; apply: dra_valid_proper. Qed.

theories/algebra/excl.v

@@ -50,16 +50,16 @@ Proof.
   - by intros [a|] [b|]; split; inversion_clear 1; constructor.
   - by intros n [a|] [b|]; split; inversion_clear 1; constructor.
 Qed.
-Canonical Structure exclC : ofeT := OfeT (excl A) excl_ofe_mixin.
+Canonical Structure exclO : ofeT := OfeT (excl A) excl_ofe_mixin.
 
-Global Instance excl_cofe `{!Cofe A} : Cofe exclC.
+Global Instance excl_cofe `{!Cofe A} : Cofe exclO.
 Proof.
   apply (iso_cofe (from_option Excl ExclBot) (maybe Excl)).
   - by intros n [a|] [b|]; split; inversion_clear 1; constructor.
   - by intros []; constructor.
 Qed.
 
-Global Instance excl_ofe_discrete : OfeDiscrete A → OfeDiscrete exclC.
+Global Instance excl_ofe_discrete : OfeDiscrete A → OfeDiscrete exclO.
 Proof. by inversion_clear 2; constructor; apply (discrete _). Qed.
 Global Instance excl_leibniz : LeibnizEquiv A → LeibnizEquiv (excl A).
 Proof. by destruct 2; f_equal; apply leibniz_equiv. Qed.
@@ -124,7 +124,7 @@ Lemma Excl_included a b : Excl' a ≼ Excl' b → a ≡ b.
 Proof. by intros [[c|] Hb%(inj Some)]; inversion_clear Hb. Qed.
 End excl.
 
-Arguments exclC : clear implicits.
+Arguments exclO : clear implicits.
 Arguments exclR : clear implicits.
 
 (* Functor *)
@@ -144,29 +144,29 @@ Proof. by intros f f' Hf; destruct 1; constructor; apply Hf. Qed.
 Instance excl_map_cmra_morphism {A B : ofeT} (f : A → B) :
   NonExpansive f → CmraMorphism (excl_map f).
 Proof. split; try done; try apply _. by intros n [a|]. Qed.
-Definition exclC_map {A B} (f : A -n> B) : exclC A -n> exclC B :=
-  CofeMor (excl_map f).
-Instance exclC_map_ne A B : NonExpansive (@exclC_map A B).
+Definition exclO_map {A B} (f : A -n> B) : exclO A -n> exclO B :=
+  OfeMor (excl_map f).
+Instance exclO_map_ne A B : NonExpansive (@exclO_map A B).
 Proof. by intros n f f' Hf []; constructor; apply Hf. Qed.
 
-Program Definition exclRF (F : cFunctor) : rFunctor := {|
-  rFunctor_car A _ B _ := (exclR (cFunctor_car F A B));
-  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := exclC_map (cFunctor_map F fg)
+Program Definition exclRF (F : oFunctor) : rFunctor := {|
+  rFunctor_car A _ B _ := (exclR (oFunctor_car F A B));
+  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := exclO_map (oFunctor_map F fg)
 |}.
 Next Obligation.
-  intros F A1 ? A2 ? B1 ? B2 ? n x1 x2 ??. by apply exclC_map_ne, cFunctor_ne.
+  intros F A1 ? A2 ? B1 ? B2 ? n x1 x2 ??. by apply exclO_map_ne, oFunctor_ne.
 Qed.
 Next Obligation.
   intros F A ? B ? x; simpl. rewrite -{2}(excl_map_id x).
-  apply excl_map_ext=>y. by rewrite cFunctor_id.
+  apply excl_map_ext=>y. by rewrite oFunctor_id.
 Qed.
 Next Obligation.
   intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl. rewrite -excl_map_compose.
-  apply excl_map_ext=>y; apply cFunctor_compose.
+  apply excl_map_ext=>y; apply oFunctor_compose.
 Qed.
 
 Instance exclRF_contractive F :
-  cFunctorContractive F → rFunctorContractive (exclRF F).
+  oFunctorContractive F → rFunctorContractive (exclRF F).
 Proof.
-  intros A1 ? A2 ? B1 ? B2 ? n x1 x2 ??. by apply exclC_map_ne, cFunctor_contractive.
+  intros A1 ? A2 ? B1 ? B2 ? n x1 x2 ??. by apply exclO_map_ne, oFunctor_contractive.
 Qed.

theories/algebra/frac.v

@@ -14,7 +14,7 @@ Set Default Proof Using "Type".
 Notation frac := Qp (only parsing).
 
 Section frac.
-Canonical Structure fracC := leibnizC frac.
+Canonical Structure fracO := leibnizO frac.
 
 Instance frac_valid : Valid frac := λ x, (x ≤ 1)%Qc.
 Instance frac_pcore : PCore frac := λ _, None.

theories/algebra/gmap.v

@@ -24,14 +24,14 @@ Proof.
     + by intros m1 m2 m3 ?? k; trans (m2 !! k).
   - by intros n m1 m2 ? k; apply dist_S.
 Qed.
-Canonical Structure gmapC : ofeT := OfeT (gmap K A) gmap_ofe_mixin.
+Canonical Structure gmapO : ofeT := OfeT (gmap K A) gmap_ofe_mixin.
 
-Program Definition gmap_chain (c : chain gmapC)
-  (k : K) : chain (optionC A) := {| chain_car n := c n !! k |}.
+Program Definition gmap_chain (c : chain gmapO)
+  (k : K) : chain (optionO A) := {| chain_car n := c n !! k |}.
 Next Obligation. by intros c k n i ?; apply (chain_cauchy c). Qed.
-Definition gmap_compl `{Cofe A} : Compl gmapC := λ c,
+Definition gmap_compl `{Cofe A} : Compl gmapO := λ c,
   map_imap (λ i _, compl (gmap_chain c i)) (c 0).
-Global Program Instance gmap_cofe `{Cofe A} : Cofe gmapC :=
+Global Program Instance gmap_cofe `{Cofe A} : Cofe gmapO :=
   {| compl := gmap_compl |}.
 Next Obligation.