diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v index 49cc8080a86caf8b04d6c324241112b754f671a1..f04343ac473fa6f81c9941ddb570026e653f1793 100644 --- a/theories/algebra/cmra.v +++ b/theories/algebra/cmra.v @@ -39,6 +39,7 @@ 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); @@ -60,6 +61,7 @@ Record CMRAMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A} := { ✓{n} x → x ≡{n}≡ y1 ⋅ y2 → ∃ z1 z2, x ≡ z1 ⋅ z2 ∧ z1 ≡{n}≡ y1 ∧ z2 ≡{n}≡ y2 }. +Unset Primitive Projections. (** Bundeled version *) Structure cmraT := CMRAT' { diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v index b5c1ef0b0a6e5b1fa408c9a772a39512d1f7887f..bba3f7a0fa95430e5e47eff0874eeb046fcd7558 100644 --- a/theories/algebra/ofe.v +++ b/theories/algebra/ofe.v @@ -33,11 +33,13 @@ 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. (** Bundeled version *) Structure ofeT := OfeT' {