Commit 782f2970 authored by Robbert Krebbers's avatar Robbert Krebbers

Some forgotten C→O renames.

parent e039d7c7
......@@ -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.
......
......@@ -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.
......@@ -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.
......
......@@ -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))).
......
......@@ -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 :=
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment