From c654a73e6c4f8607d463e34a69d545b30c2e2850 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 10 Oct 2017 13:34:03 +0200
Subject: [PATCH] use primitive projections for our mixins

---
 theories/algebra/cmra.v | 2 ++
 theories/algebra/ofe.v  | 2 ++
 2 files changed, 4 insertions(+)

diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 49cc8080a..f04343ac4 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 b5c1ef0b0..bba3f7a0f 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' {
-- 
GitLab