From a19d201e67ece195c33d004e6181a7a8510c16cd Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Tue, 10 Oct 2017 14:56:51 +0200 Subject: [PATCH] use sections to scope options --- theories/algebra/cmra.v | 47 +++++++++++++++++++++-------------------- theories/algebra/ofe.v | 15 +++++++------ 2 files changed, 32 insertions(+), 30 deletions(-) diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v index f04343ac..85c785d2 100644 --- a/theories/algebra/cmra.v +++ b/theories/algebra/cmra.v @@ -39,29 +39,30 @@ Notation "x ≼{ n } y" := (includedN n x y) Instance: Params (@includedN) 4. Hint Extern 0 (_ ≼{_} _) => reflexivity. -Set Primitive Projections. -Record CMRAMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A} := { - (* setoids *) - mixin_cmra_op_ne (x : A) : NonExpansive (op x); - mixin_cmra_pcore_ne n x y cx : - x ≡{n}≡ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≡{n}≡ cy; - mixin_cmra_validN_ne n : Proper (dist n ==> impl) (validN n); - (* valid *) - mixin_cmra_valid_validN x : ✓ x ↔ ∀ n, ✓{n} x; - mixin_cmra_validN_S n x : ✓{S n} x → ✓{n} x; - (* monoid *) - mixin_cmra_assoc : Assoc (≡) (⋅); - mixin_cmra_comm : Comm (≡) (⋅); - mixin_cmra_pcore_l x cx : pcore x = Some cx → cx ⋅ x ≡ x; - mixin_cmra_pcore_idemp x cx : pcore x = Some cx → pcore cx ≡ Some cx; - mixin_cmra_pcore_mono x y cx : - x ≼ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼ cy; - mixin_cmra_validN_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x; - mixin_cmra_extend n x y1 y2 : - ✓{n} x → x ≡{n}≡ y1 ⋅ y2 → - ∃ z1 z2, x ≡ z1 ⋅ z2 ∧ z1 ≡{n}≡ y1 ∧ z2 ≡{n}≡ y2 -}. -Unset Primitive Projections. +Section mixin. + Local Set Primitive Projections. + Record CMRAMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A} := { + (* setoids *) + mixin_cmra_op_ne (x : A) : NonExpansive (op x); + mixin_cmra_pcore_ne n x y cx : + x ≡{n}≡ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≡{n}≡ cy; + mixin_cmra_validN_ne n : Proper (dist n ==> impl) (validN n); + (* valid *) + mixin_cmra_valid_validN x : ✓ x ↔ ∀ n, ✓{n} x; + mixin_cmra_validN_S n x : ✓{S n} x → ✓{n} x; + (* monoid *) + mixin_cmra_assoc : Assoc (≡) (⋅); + mixin_cmra_comm : Comm (≡) (⋅); + mixin_cmra_pcore_l x cx : pcore x = Some cx → cx ⋅ x ≡ x; + mixin_cmra_pcore_idemp x cx : pcore x = Some cx → pcore cx ≡ Some cx; + mixin_cmra_pcore_mono x y cx : + x ≼ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼ cy; + mixin_cmra_validN_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x; + mixin_cmra_extend n x y1 y2 : + ✓{n} x → x ≡{n}≡ y1 ⋅ y2 → + ∃ z1 z2, x ≡ z1 ⋅ z2 ∧ z1 ≡{n}≡ y1 ∧ z2 ≡{n}≡ y2 + }. +End mixin. (** Bundeled version *) Structure cmraT := CMRAT' { diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v index bba3f7a0..09992145 100644 --- a/theories/algebra/ofe.v +++ b/theories/algebra/ofe.v @@ -33,13 +33,14 @@ Tactic Notation "ofe_subst" := | H:@dist ?A ?d ?n _ ?x |- _ => symmetry in H;setoid_subst_aux (@dist A d n) x end. -Set Primitive Projections. -Record OfeMixin A `{Equiv A, Dist A} := { - mixin_equiv_dist x y : x ≡ y ↔ ∀ n, x ≡{n}≡ y; - mixin_dist_equivalence n : Equivalence (dist n); - mixin_dist_S n x y : x ≡{S n}≡ y → x ≡{n}≡ y -}. -Unset Primitive Projections. +Section mixin. + Local Set Primitive Projections. + Record OfeMixin A `{Equiv A, Dist A} := { + mixin_equiv_dist x y : x ≡ y ↔ ∀ n, x ≡{n}≡ y; + mixin_dist_equivalence n : Equivalence (dist n); + mixin_dist_S n x y : x ≡{S n}≡ y → x ≡{n}≡ y + }. +End mixin. (** Bundeled version *) Structure ofeT := OfeT' { -- GitLab