From d4a9c75dea8a7ce53981cf8089eb9552dce86f4e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 14 Nov 2017 01:45:06 +0100
Subject: [PATCH] Enable primitive projections for OFEs.

---
 theories/algebra/auth.v  |  4 ++--
 theories/algebra/cmra.v  | 12 ++++++------
 theories/algebra/iprod.v |  5 ++++-
 theories/algebra/ofe.v   | 24 ++++++++++--------------
 4 files changed, 22 insertions(+), 23 deletions(-)

diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index 607d0cae2..a5f62158a 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -154,7 +154,7 @@ Proof.
   - by split; simpl; rewrite ?cmra_core_l.
   - by split; simpl; rewrite ?cmra_core_idemp.
   - intros ??; rewrite! auth_included; intros [??].
-    by split; simpl; apply cmra_core_mono.
+    by split; simpl; apply: cmra_core_mono. (* FIXME: apply cmra_core_mono. fails *)
   - assert (∀ n (a b1 b2 : A), b1 ⋅ b2 ≼{n} a → b1 ≼{n} a).
     { intros n a b1 b2 <-; apply cmra_includedN_l. }
    intros n [[[a1|]|] b1] [[[a2|]|] b2]; rewrite auth_validN_eq;
@@ -208,7 +208,7 @@ Lemma auth_frag_mono a b : a ≼ b → ◯ a ≼ ◯ b.
 Proof. intros [c ->]. rewrite auth_frag_op. apply cmra_included_l. Qed.
 
 Global Instance auth_frag_sep_homomorphism :
-  MonoidHomomorphism op op (≡) (Auth None).
+  MonoidHomomorphism op op (≡) (@Auth A None).
 Proof. by split; [split; try apply _|]. Qed.
 
 Lemma auth_both_op a b : Auth (Excl' a) b ≡ ● a ⋅ ◯ b.
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 3c3b1171c..c60a19c35 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -1230,7 +1230,7 @@ Qed.
 (** ** CMRA for the option type *)
 Section option.
   Context {A : cmraT}.
-  Implicit Types a : A.
+  Implicit Types x y : A.
   Local Arguments core _ _ !_ /.
   Local Arguments pcore _ _ !_ /.
 
@@ -1242,11 +1242,11 @@ Section option.
   Arguments option_pcore !_ /.
   Instance option_op : Op (option A) := union_with (λ x y, Some (x ⋅ y)).
 
-  Definition Some_valid a : ✓ Some a ↔ ✓ a := reflexivity _.
-  Definition Some_validN a n : ✓{n} Some a ↔ ✓{n} a := reflexivity _.
-  Definition Some_op a b : Some (a â‹… b) = Some a â‹… Some b := eq_refl.
-  Lemma Some_core `{CmraTotal A} a : Some (core a) = core (Some a).
-  Proof. rewrite /core /=. by destruct (cmra_total a) as [? ->]. Qed.
+  Definition Some_valid x : ✓ Some x ↔ ✓ x := reflexivity _.
+  Definition Some_validN x n : ✓{n} Some x ↔ ✓{n} x := reflexivity _.
+  Definition Some_op x y : Some (x â‹… y) = Some x â‹… Some y := eq_refl.
+  Lemma Some_core `{CmraTotal A} x : Some (core x) = core (Some x).
+  Proof. rewrite /core /=. by destruct (cmra_total x) as [? ->]. Qed.
   Lemma Some_op_opM x my : Some x â‹… my = Some (x â‹…? my).
   Proof. by destruct my. Qed.
 
diff --git a/theories/algebra/iprod.v b/theories/algebra/iprod.v
index e3051d27f..c45034013 100644
--- a/theories/algebra/iprod.v
+++ b/theories/algebra/iprod.v
@@ -318,7 +318,10 @@ Instance iprodCF_contractive `{Finite C} (F : C → cFunctor) :
   (∀ c, cFunctorContractive (F c)) → cFunctorContractive (iprodCF F).
 Proof.
   intros ? A1 A2 B1 B2 n ?? g.
-  by apply iprodC_map_ne=>c; apply cFunctor_contractive.
+  (* FIXME: when using `apply` we get
+    Anomaly "Uncaught exception Retyping.RetypeError(4)." Please report at http://coq.inria.fr/bugs/.
+  *)
+  apply: iprodC_map_ne=>c. by apply cFunctor_contractive.
 Qed.
 
 Program Definition iprodURF `{Finite C} (F : C → urFunctor) : urFunctor := {|
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 9997c5c4b..f7c2460a1 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -1,5 +1,6 @@
 From iris.algebra Require Export base.
 Set Default Proof Using "Type".
+Set Primitive Projections.
 
 (** This files defines (a shallow embedding of) the category of OFEs:
     Complete ordered families of equivalences. This is a cartesian closed
@@ -33,25 +34,20 @@ Tactic Notation "ofe_subst" :=
   | H:@dist ?A ?d ?n _ ?x |- _ => symmetry in H;setoid_subst_aux (@dist A d n) x
   end.
 
-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.
+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
+}.
 
 (** Bundeled version *)
-Structure ofeT := OfeT' {
+Structure ofeT := OfeT {
   ofe_car :> Type;
   ofe_equiv : Equiv ofe_car;
   ofe_dist : Dist ofe_car;
-  ofe_mixin : OfeMixin ofe_car;
-  _ : Type
+  ofe_mixin : OfeMixin ofe_car
 }.
-Arguments OfeT' _ {_ _} _ _.
-Notation OfeT A m := (OfeT' A m A).
+Arguments OfeT _ {_ _} _.
 Add Printing Constructor ofeT.
 Hint Extern 0 (Equiv _) => eapply (@ofe_equiv _) : typeclass_instances.
 Hint Extern 0 (Dist _) => eapply (@ofe_dist _) : typeclass_instances.
@@ -1057,7 +1053,7 @@ Proof.
 Qed.
 
 (** Later *)
-Inductive later (A : Type) : Type := Next { later_car : A }.
+Record later (A : Type) : Type := Next { later_car : A }.
 Add Printing Constructor later.
 Arguments Next {_} _.
 Arguments later_car {_} _.
-- 
GitLab