Smarter constructors for ofeT, cmraT and ucmraT.

theories/algebra/agree.v

@@ -318,8 +318,7 @@ Proof.
     + by rewrite agree_idemp.
     + by move: Hval; rewrite Hx; move=> /agree_op_invN->; rewrite agree_idemp.
 Qed.
-Canonical Structure agreeR : cmraT :=
-  CMRAT (agree A) agree_ofe_mixin agree_cmra_mixin.
+Canonical Structure agreeR : cmraT := CMRAT (agree A) agree_cmra_mixin.
 
 Global Instance agree_total : CMRATotal agreeR.
 Proof. rewrite /CMRATotal; eauto. Qed.

theories/algebra/auth.v

@@ -175,7 +175,7 @@ Proof.
       as (b1&b2&?&?&?); auto using auth_own_validN.
     by exists (Auth ea1 b1), (Auth ea2 b2).
 Qed.
-Canonical Structure authR := CMRAT (auth A) auth_ofe_mixin auth_cmra_mixin.
+Canonical Structure authR := CMRAT (auth A) auth_cmra_mixin.
 
 Global Instance auth_cmra_discrete : CMRADiscrete A → CMRADiscrete authR.
 Proof.
@@ -194,8 +194,7 @@ Proof.
   - by intros x; constructor; rewrite /= left_id.
   - do 2 constructor; simpl; apply (persistent_core _).
 Qed.
-Canonical Structure authUR :=
-  UCMRAT (auth A) auth_ofe_mixin auth_cmra_mixin auth_ucmra_mixin.
+Canonical Structure authUR := UCMRAT (auth A) auth_ucmra_mixin.
 
 Global Instance auth_frag_persistent a : Persistent a → Persistent (◯ a).
 Proof. do 2 constructor; simpl; auto. by apply persistent_core. Qed.

theories/algebra/cmra.v

@@ -71,7 +71,11 @@ Structure cmraT := CMRAT' {
   _ : Type
 }.
 Arguments CMRAT' _ {_ _ _ _ _ _} _ _ _.
-Notation CMRAT A m m' := (CMRAT' A m m' A).
+(* Given [m : CMRAMixin A], the notation [CMRAT A m] provides a smart
+constructor, which uses [ofe_mixin_of A] to infer the canonical OFE mixin of
+the type [A], so that it does not have to be given manually. *)
+Notation CMRAT A m := (CMRAT' A (ofe_mixin_of A%type) m A) (only parsing).
+
 Arguments cmra_car : simpl never.
 Arguments cmra_equiv : simpl never.
 Arguments cmra_dist : simpl never.
@@ -89,6 +93,10 @@ Hint Extern 0 (ValidN _) => eapply (@cmra_validN _) : typeclass_instances.
 Coercion cmra_ofeC (A : cmraT) : ofeT := OfeT A (cmra_ofe_mixin A).
 Canonical Structure cmra_ofeC.
 
+Definition cmra_mixin_of' A {Ac : cmraT} (f : Ac → A) : CMRAMixin Ac := cmra_mixin Ac.
+Notation cmra_mixin_of A :=
+  ltac:(let H := eval hnf in (cmra_mixin_of' A id) in exact H) (only parsing).
+
 (** Lifting properties from the mixin *)
 Section cmra_mixin.
   Context {A : cmraT}.
@@ -184,7 +192,8 @@ Structure ucmraT := UCMRAT' {
   _ : Type;
 }.
 Arguments UCMRAT' _ {_ _ _ _ _ _ _} _ _ _ _.
-Notation UCMRAT A m m' m'' := (UCMRAT' A m m' m'' A).
+Notation UCMRAT A m :=
+  (UCMRAT' A (ofe_mixin_of A%type) (cmra_mixin_of A%type) m A) (only parsing).
 Arguments ucmra_car : simpl never.
 Arguments ucmra_equiv : simpl never.
 Arguments ucmra_dist : simpl never.
@@ -200,7 +209,7 @@ Hint Extern 0 (Empty _) => eapply (@ucmra_empty _) : typeclass_instances.
 Coercion ucmra_ofeC (A : ucmraT) : ofeT := OfeT A (ucmra_ofe_mixin A).
 Canonical Structure ucmra_ofeC.
 Coercion ucmra_cmraR (A : ucmraT) : cmraT :=
-  CMRAT A (ucmra_ofe_mixin A) (ucmra_cmra_mixin A).
+  CMRAT' A (ucmra_ofe_mixin A) (ucmra_cmra_mixin A) A.
 Canonical Structure ucmra_cmraR.
 
 (** Lifting properties from the mixin *)
@@ -862,7 +871,7 @@ Record RAMixin A `{Equiv A, PCore A, Op A, Valid A} := {
 
 Section discrete.
   Local Set Default Proof Using "Type*".
-  Context `{Equiv A, PCore A, Op A, Valid A, @Equivalence A (≡)}.
+  Context `{Equiv A, PCore A, Op A, Valid A} (Heq : @Equivalence A (≡)).
   Context (ra_mix : RAMixin A).
   Existing Instances discrete_dist.
 
@@ -873,16 +882,18 @@ Section discrete.
     - intros x; split; first done. by move=> /(_ 0).
     - intros n x y1 y2 ??; by exists y1, y2.
   Qed.
+
+  Instance discrete_cmra_discrete :
+    CMRADiscrete (CMRAT' A (discrete_ofe_mixin Heq) discrete_cmra_mixin A).
+  Proof. split. apply _. done. Qed.
 End discrete.
 
+(** A smart constructor for the discrete RA over a carrier [A]. It uses
+[discrete_ofe_equivalence_of A] to make sure the same [Equivalence] proof is
+used as when constructing the OFE. *)
 Notation discreteR A ra_mix :=
-  (CMRAT A discrete_ofe_mixin (discrete_cmra_mixin ra_mix)).
-Notation discreteUR A ra_mix ucmra_mix :=
-  (UCMRAT A discrete_ofe_mixin (discrete_cmra_mixin ra_mix) ucmra_mix).
-
-Global Instance discrete_cmra_discrete `{Equiv A, PCore A, Op A, Valid A,
-  @Equivalence A (≡)} (ra_mix : RAMixin A) : CMRADiscrete (discreteR A ra_mix).
-Proof. split. apply _. done. Qed.
+  (CMRAT A (discrete_cmra_mixin (discrete_ofe_equivalence_of A%type) ra_mix))
+  (only parsing).
 
 Section ra_total.
   Local Set Default Proof Using "Type*".
@@ -918,13 +929,12 @@ Section unit.
   Instance unit_op : Op () := λ x y, ().
   Lemma unit_cmra_mixin : CMRAMixin ().
   Proof. apply discrete_cmra_mixin, ra_total_mixin; by eauto. Qed.
-  Canonical Structure unitR : cmraT := CMRAT () unit_ofe_mixin unit_cmra_mixin.
+  Canonical Structure unitR : cmraT := CMRAT unit unit_cmra_mixin.
 
   Instance unit_empty : Empty () := ().
   Lemma unit_ucmra_mixin : UCMRAMixin ().
   Proof. done. Qed.
-  Canonical Structure unitUR : ucmraT :=
-    UCMRAT () unit_ofe_mixin unit_cmra_mixin unit_ucmra_mixin.
+  Canonical Structure unitUR : ucmraT := UCMRAT unit unit_ucmra_mixin.
 
   Global Instance unit_cmra_discrete : CMRADiscrete unitR.
   Proof. done. Qed.
@@ -957,14 +967,13 @@ Section nat.
   Qed.
   Canonical Structure natR : cmraT := discreteR nat nat_ra_mixin.
 
+  Global Instance nat_cmra_discrete : CMRADiscrete natR.
+  Proof. apply discrete_cmra_discrete. Qed.
+
   Instance nat_empty : Empty nat := 0.
   Lemma nat_ucmra_mixin : UCMRAMixin nat.
   Proof. split; apply _ || done. Qed.
-  Canonical Structure natUR : ucmraT :=
-    discreteUR nat nat_ra_mixin nat_ucmra_mixin.
-
-  Global Instance nat_cmra_discrete : CMRADiscrete natR.
-  Proof. constructor; apply _ || done. Qed.
+  Canonical Structure natUR : ucmraT := UCMRAT nat nat_ucmra_mixin.
 
   Global Instance nat_cancelable (x : nat) : Cancelable x.
   Proof. by intros ???? ?%Nat.add_cancel_l. Qed.
@@ -995,14 +1004,14 @@ Section mnat.
   Qed.
   Canonical Structure mnatR : cmraT := discreteR mnat mnat_ra_mixin.
 
+  Global Instance mnat_cmra_discrete : CMRADiscrete mnatR.
+  Proof. apply discrete_cmra_discrete. Qed.
+
   Instance mnat_empty : Empty mnat := 0.
   Lemma mnat_ucmra_mixin : UCMRAMixin mnat.
   Proof. split; apply _ || done. Qed.
-  Canonical Structure mnatUR : ucmraT :=
-    discreteUR mnat mnat_ra_mixin mnat_ucmra_mixin.
+  Canonical Structure mnatUR : ucmraT := UCMRAT mnat mnat_ucmra_mixin.
 
-  Global Instance mnat_cmra_discrete : CMRADiscrete mnatR.
-  Proof. constructor; apply _ || done. Qed.
   Global Instance mnat_persistent (x : mnat) : Persistent x.
   Proof. by constructor. Qed.
 End mnat.
@@ -1030,7 +1039,8 @@ Section positive.
   Canonical Structure positiveR : cmraT := discreteR positive pos_ra_mixin.
 
   Global Instance pos_cmra_discrete : CMRADiscrete positiveR.
-  Proof. constructor; apply _ || done. Qed.
+  Proof. apply discrete_cmra_discrete. Qed.
+
   Global Instance pos_cancelable (x : positive) : Cancelable x.
   Proof. intros n y z ??. by eapply Pos.add_reg_l, leibniz_equiv. Qed.
   Global Instance pos_id_free (x : positive) : IdFree x.
@@ -1105,8 +1115,7 @@ Section prod.
       destruct (cmra_extend n (x.2) (y1.2) (y2.2)) as (z21&z22&?&?&?); auto.
       by exists (z11,z21), (z12,z22).
   Qed.
-  Canonical Structure prodR :=
-    CMRAT (A * B) prod_ofe_mixin prod_cmra_mixin.
+  Canonical Structure prodR := CMRAT (prod A B) prod_cmra_mixin.
 
   Lemma pair_op (a a' : A) (b b' : B) : (a, b) ⋅ (a', b') = (a ⋅ a', b ⋅ b').
   Proof. done. Qed.
@@ -1153,8 +1162,7 @@ Section prod_unit.
     - by split; rewrite /=left_id.
     - rewrite prod_pcore_Some'; split; apply (persistent _).
   Qed.
-  Canonical Structure prodUR :=
-    UCMRAT (A * B) prod_ofe_mixin prod_cmra_mixin prod_ucmra_mixin.
+  Canonical Structure prodUR := UCMRAT (prod A B) prod_ucmra_mixin.
 
   Lemma pair_split (x : A) (y : B) : (x, y) ≡ (x, ∅) ⋅ (∅, y).
   Proof. by rewrite pair_op left_id right_id. Qed.
@@ -1289,8 +1297,7 @@ Section option.
       + by exists None, (Some x); repeat constructor.
       + exists None, None; repeat constructor.
   Qed.
-  Canonical Structure optionR :=
-    CMRAT (option A) option_ofe_mixin option_cmra_mixin.
+  Canonical Structure optionR := CMRAT (option A) option_cmra_mixin.
 
   Global Instance option_cmra_discrete : CMRADiscrete A → CMRADiscrete optionR.
   Proof. split; [apply _|]. by intros [x|]; [apply (cmra_discrete_valid x)|]. Qed.
@@ -1298,8 +1305,7 @@ Section option.
   Instance option_empty : Empty (option A) := None.
   Lemma option_ucmra_mixin : UCMRAMixin optionR.
   Proof. split. done. by intros []. done. Qed.
-  Canonical Structure optionUR :=
-    UCMRAT (option A) option_ofe_mixin option_cmra_mixin option_ucmra_mixin.
+  Canonical Structure optionUR := UCMRAT (option A) option_ucmra_mixin.
 
   (** Misc *)
   Global Instance Some_cmra_monotone : CMRAMonotone Some.

theories/algebra/coPset.v

@@ -38,10 +38,12 @@ Section coPset.
   Qed.
   Canonical Structure coPsetR := discreteR coPset coPset_ra_mixin.
 
+  Global Instance coPset_cmra_discrete : CMRADiscrete coPsetR.
+  Proof. apply discrete_cmra_discrete. Qed.
+
   Lemma coPset_ucmra_mixin : UCMRAMixin coPset.
   Proof. split. done. intros X. by rewrite coPset_op_union left_id_L. done. Qed.
-  Canonical Structure coPsetUR :=
-    discreteUR coPset coPset_ra_mixin coPset_ucmra_mixin.
+  Canonical Structure coPsetUR := UCMRAT coPset coPset_ucmra_mixin.
 
   Lemma coPset_opM X mY : X ⋅? mY = X ∪ from_option id ∅ mY.
   Proof. destruct mY; by rewrite /= ?right_id_L. Qed.
@@ -109,8 +111,10 @@ Section coPset_disj.
   Qed.
   Canonical Structure coPset_disjR := discreteR coPset_disj coPset_disj_ra_mixin.
 
+  Global Instance coPset_disj_cmra_discrete : CMRADiscrete coPset_disjR.
+  Proof. apply discrete_cmra_discrete. Qed.
+
   Lemma coPset_disj_ucmra_mixin : UCMRAMixin coPset_disj.
   Proof. split; try apply _ || done. intros [X|]; coPset_disj_solve. Qed.
-  Canonical Structure coPset_disjUR :=
-    discreteUR coPset_disj coPset_disj_ra_mixin coPset_disj_ucmra_mixin.
+  Canonical Structure coPset_disjUR := UCMRAT coPset_disj coPset_disj_ucmra_mixin.
 End coPset_disj.

theories/algebra/csum.v

@@ -246,8 +246,7 @@ Proof.
       exists (Cinr z1), (Cinr z2). by repeat constructor.
     + by exists CsumBot, CsumBot; destruct y1, y2; inversion_clear Hx'.
 Qed.
-Canonical Structure csumR :=
-  CMRAT (csum A B) csum_ofe_mixin csum_cmra_mixin.
+Canonical Structure csumR := CMRAT (csum A B) csum_cmra_mixin.
 
 Global Instance csum_cmra_discrete :
   CMRADiscrete A → CMRADiscrete B → CMRADiscrete csumR.

theories/algebra/dra.v

@@ -177,6 +177,8 @@ Qed.
 Canonical Structure validityR : cmraT :=
   discreteR (validity A) validity_ra_mixin.
 
+Global Instance validity_cmra_disrete : CMRADiscrete validityR.
+Proof. apply discrete_cmra_discrete. Qed.
 Global Instance validity_cmra_total : CMRATotal validityR.
 Proof. rewrite /CMRATotal; eauto. Qed.
 

theories/algebra/excl.v

@@ -101,8 +101,7 @@ Proof.
   - by intros n [?|] [?|].
   - intros n x [?|] [?|] ?; inversion_clear 1; eauto.
 Qed.
-Canonical Structure exclR :=
-  CMRAT (excl A) excl_ofe_mixin excl_cmra_mixin.
+Canonical Structure exclR := CMRAT (excl A) excl_cmra_mixin.
 
 Global Instance excl_cmra_discrete : Discrete A → CMRADiscrete exclR.
 Proof. split. apply _. by intros []. Qed.

theories/algebra/frac.v

@@ -29,6 +29,9 @@ Proof.
   rewrite -{1}(Qcplus_0_r x) -Qcplus_le_mono_l; auto using Qclt_le_weak.
 Qed.
 Canonical Structure fracR := discreteR frac frac_ra_mixin.
+
+Global Instance frac_cmra_discrete : CMRADiscrete fracR.
+Proof. apply discrete_cmra_discrete. Qed.
 End frac.
 
 Global Instance frac_full_exclusive : Exclusive 1%Qp.

theories/algebra/gmap.v

@@ -170,8 +170,7 @@ Proof.
       * by rewrite lookup_partial_alter.
       * by rewrite lookup_partial_alter_ne // Hm2' lookup_delete_ne.
 Qed.
-Canonical Structure gmapR :=
-  CMRAT (gmap K A) gmap_ofe_mixin gmap_cmra_mixin.
+Canonical Structure gmapR := CMRAT (gmap K A) gmap_cmra_mixin.
 
 Global Instance gmap_cmra_discrete : CMRADiscrete A → CMRADiscrete gmapR.
 Proof. split; [apply _|]. intros m ? i. by apply: cmra_discrete_valid. Qed.
@@ -183,8 +182,7 @@ Proof.
   - by intros m i; rewrite /= lookup_op lookup_empty (left_id_L None _).
   - constructor=> i. by rewrite lookup_omap lookup_empty.
 Qed.
-Canonical Structure gmapUR :=
-  UCMRAT (gmap K A) gmap_ofe_mixin gmap_cmra_mixin gmap_ucmra_mixin.
+Canonical Structure gmapUR := UCMRAT (gmap K A) gmap_ucmra_mixin.
 
 (** Internalized properties *)
 Lemma gmap_equivI {M} m1 m2 : m1 ≡ m2 ⊣⊢ (∀ i, m1 !! i ≡ m2 !! i : uPred M).

theories/algebra/gset.v

@@ -37,10 +37,12 @@ Section gset.
   Qed.
   Canonical Structure gsetR := discreteR (gset K) gset_ra_mixin.
 
+  Global Instance gset_cmra_discrete : CMRADiscrete gsetR.
+  Proof. apply discrete_cmra_discrete. Qed.
+
   Lemma gset_ucmra_mixin : UCMRAMixin (gset K).
   Proof. split. done. intros X. by rewrite gset_op_union left_id_L. done. Qed.
-  Canonical Structure gsetUR :=
-    discreteUR (gset K) gset_ra_mixin gset_ucmra_mixin.
+  Canonical Structure gsetUR := UCMRAT (gset K) gset_ucmra_mixin.
 
   Lemma gset_opM X mY : X ⋅? mY = X ∪ from_option id ∅ mY.
   Proof. destruct mY; by rewrite /= ?right_id_L. Qed.
@@ -120,10 +122,12 @@ Section gset_disj.
   Qed.
   Canonical Structure gset_disjR := discreteR (gset_disj K) gset_disj_ra_mixin.
 
+  Global Instance gset_disj_cmra_discrete : CMRADiscrete gset_disjR.
+  Proof. apply discrete_cmra_discrete. Qed.
+
   Lemma gset_disj_ucmra_mixin : UCMRAMixin (gset_disj K).
   Proof. split; try apply _ || done. intros [X|]; gset_disj_solve. Qed.
-  Canonical Structure gset_disjUR :=
-    discreteUR (gset_disj K) gset_disj_ra_mixin gset_disj_ucmra_mixin.
+  Canonical Structure gset_disjUR := UCMRAT (gset_disj K) gset_disj_ucmra_mixin.
 
   Arguments op _ _ _ _ : simpl never.
 

theories/algebra/iprod.v

@@ -126,8 +126,7 @@ Section iprod_cmra.
         exists (y1,y2); eauto. }
       exists (λ x, gg x.1), (λ x, gg x.2). split_and!=> -?; naive_solver.
   Qed.
-  Canonical Structure iprodR :=
-    CMRAT (iprod B) iprod_ofe_mixin iprod_cmra_mixin.
+  Canonical Structure iprodR := CMRAT (iprod B) iprod_cmra_mixin.
 
   Instance iprod_empty : Empty (iprod B) := λ x, ∅.
   Definition iprod_lookup_empty x : ∅ x = ∅ := eq_refl.
@@ -139,8 +138,7 @@ Section iprod_cmra.
     - by intros f x; rewrite iprod_lookup_op left_id.
     - constructor=> x. apply persistent_core, _.
   Qed.
-  Canonical Structure iprodUR :=
-    UCMRAT (iprod B) iprod_ofe_mixin iprod_cmra_mixin iprod_ucmra_mixin.
+  Canonical Structure iprodUR := UCMRAT (iprod B) iprod_ucmra_mixin.
 
   Global Instance iprod_empty_timeless :
     (∀ i, Timeless (∅ : B i)) → Timeless (∅ : iprod B).

theories/algebra/list.v

@@ -219,7 +219,7 @@ Section cmra.
           (cmra_extend n x y1 y2) as (y1'&y2'&?&?&?); simplify_eq/=; auto.
         exists (y1' :: l1'), (y2' :: l2'); repeat constructor; auto.
   Qed.
-  Canonical Structure listR := CMRAT (list A) list_ofe_mixin list_cmra_mixin.
+  Canonical Structure listR := CMRAT (list A) list_cmra_mixin.
 
   Global Instance empty_list : Empty (list A) := [].
   Definition list_ucmra_mixin : UCMRAMixin (list A).
@@ -229,8 +229,7 @@ Section cmra.
     - by intros l.
     - by constructor.
   Qed.
-  Canonical Structure listUR :=
-    UCMRAT (list A) list_ofe_mixin list_cmra_mixin list_ucmra_mixin.
+  Canonical Structure listUR := UCMRAT (list A) list_ucmra_mixin.
 
   Global Instance list_cmra_discrete : CMRADiscrete A → CMRADiscrete listR.
   Proof.

theories/algebra/ofe.v

@@ -57,6 +57,31 @@ Arguments ofe_equiv : simpl never.
 Arguments ofe_dist : simpl never.
 Arguments ofe_mixin : simpl never.
 
+(** When declaring instances of subclasses of OFE (like CMRAs and unital CMRAs)
+we need Coq to *infer* the canonical OFE instance of a given type and take the
+mixin out of it. This makes sure we do not use two different OFE instances in
+different places (see for example the constructors [CMRAT] and [UCMRAT] in the
+file [cmra.v].)
+
+In order to infer the OFE instance, we use the definition [ofe_mixin_of'] which
+is inspired by the [clone] trick in ssreflect. It works as follows, when type
+checking [@ofe_mixin_of' A ?Ac id] Coq faces a unification problem:
+
+  ofe_car ?Ac  ~  A
+
+which will resolve [?Ac] to the canonical OFE instance corresponding to [A]. The
+definition [@ofe_mixin_of' A ?Ac id] will then provide the corresponding mixin.
+Note that type checking of [ofe_mixin_of' A id] will fail when [A] does not have
+a canonical OFE instance.
+
+The notation [ofe_mixin_of A] that we define on top of [ofe_mixin_of' A id]
+hides the [id] and normalizes the mixin to head normal form. The latter is to
+ensure that we do not end up with redundant canonical projections to the mixin,
+i.e. them all being of the shape [ofe_mixin_of' A id]. *)
+Definition ofe_mixin_of' A {Ac : ofeT} (f : Ac → A) : OfeMixin Ac := ofe_mixin Ac.
+Notation ofe_mixin_of A :=
+  ltac:(let H := eval hnf in (ofe_mixin_of' A id) in exact H) (only parsing).
+
 (** Lifting properties from the mixin *)
 Section ofe_mixin.
   Context {A : ofeT}.
@@ -100,8 +125,7 @@ Class Cofe (A : ofeT) := {
 }.
 Arguments compl : simpl never.
 
-Lemma compl_chain_map `{Cofe A, Cofe B} (f : A → B) c
-      `(NonExpansive f) :
+Lemma compl_chain_map `{Cofe A, Cofe B} (f : A → B) c `(NonExpansive f) :
   compl (chain_map f c) ≡ f (compl c).
 Proof. apply equiv_dist=>n. by rewrite !conv_compl. Qed.
 
@@ -109,7 +133,7 @@ Proof. apply equiv_dist=>n. by rewrite !conv_compl. Qed.
 Section cofe.
   Context {A : ofeT}.
   Implicit Types x y : A.
-  Global Instance cofe_equivalence : Equivalence ((≡) : relation A).
+  Global Instance ofe_equivalence : Equivalence ((≡) : relation A).
   Proof.
     split.
     - by intros x; rewrite equiv_dist.
@@ -784,7 +808,7 @@ Qed.
 
 (** Discrete cofe *)
 Section discrete_cofe.
-  Context `{Equiv A, @Equivalence A (≡)}.
+  Context `{Equiv A} (Heq : @Equivalence A (≡)).
 
   Instance discrete_dist : Dist A := λ n x y, x ≡ y.
   Definition discrete_ofe_mixin : OfeMixin A.
@@ -795,6 +819,9 @@ Section discrete_cofe.
     - done.
   Qed.
 
+  Global Instance discrete_discrete_ofe : Discrete (OfeT A discrete_ofe_mixin).
+  Proof. by intros x y. Qed.
+
   Global Program Instance discrete_cofe : Cofe (OfeT A discrete_ofe_mixin) :=
     { compl c := c 0 }.
   Next Obligation.
@@ -803,12 +830,22 @@ Section discrete_cofe.
   Qed.
 End discrete_cofe.
 
-Notation discreteC A := (OfeT A discrete_ofe_mixin).
+Notation discreteC A := (OfeT A (discrete_ofe_mixin _)).
 Notation leibnizC A := (OfeT A (@discrete_ofe_mixin _ equivL _)).
 
-Instance discrete_discrete_cofe `{Equiv A, @Equivalence A (≡)} :
-  Discrete (discreteC A).
-Proof. by intros x y. Qed.
+(** In order to define a discrete CMRA with carrier [A] (in the file [cmra.v])
+we need to determine the [Equivalence A] proof that was used to construct the
+OFE instance of [A] (note that this proof is not the same as the one we obtain
+via [ofe_equivalence]).
+
+We obtain the proof of [Equivalence A] by inferring the canonical OFE mixin
+using [ofe_mixin_of A], and then check whether it is indeed a discrete OFE. This
+will fail if no OFE, or an OFE other than the discrete OFE, was registered. *)
+Notation discrete_ofe_equivalence_of A := ltac:(
+  match constr:(ofe_mixin_of A) with
+  | discrete_ofe_mixin ?H => exact H
+  end) (only parsing).
+
 Instance leibnizC_leibniz A : LeibnizEquiv (leibnizC A).
 Proof. by intros x y. Qed.
 

theories/base_logic/big_op.v

@@ -52,8 +52,7 @@ Section cmra.
         by rewrite left_id.
   Qed.
 
-  Canonical Structure uPredR :=
-    CMRAT (uPred M) uPred_ofe_mixin uPred_cmra_mixin.
+  Canonical Structure uPredR := CMRAT (uPred M) uPred_cmra_mixin.
 
   Instance uPred_empty : Empty (uPred M) := True%I.
 
@@ -64,8 +63,7 @@ Section cmra.
     - intros P. by rewrite left_id.
   Qed.
 
-  Canonical Structure uPredUR :=
-    UCMRAT (uPred M) uPred_ofe_mixin uPred_cmra_mixin uPred_ucmra_mixin.
+  Canonical Structure uPredUR := UCMRAT (uPred M) uPred_ucmra_mixin.
 
   Global Instance uPred_always_homomorphism : UCMRAHomomorphism uPred_always.
   Proof. split; [split|]. apply _. apply always_sep. apply always_pure. Qed.

theories/tests/ipm_paper.v

@@ -151,12 +151,16 @@ Section M.
     - intros [n1|i1|] [n2|i2|]; simpl; by try case_decide.
   Qed.
   Canonical Structure M_R : cmraT := discreteR M M_ra_mixin.
+
+  Global Instance M_cmra_discrete : CMRADiscrete M_R.
+  Proof. apply discrete_cmra_discrete. Qed.
+
   Definition M_ucmra_mixin : UCMRAMixin M.
   Proof.
     split; try (done || apply _).
     intros [?|?|]; simpl; try case_decide; f_equal/=; lia.
   Qed.
-  Canonical Structure M_UR : ucmraT := discreteUR M M_ra_mixin M_ucmra_mixin.
+  Canonical Structure M_UR : ucmraT := UCMRAT M M_ucmra_mixin.
 
   Global Instance frag_persistent n : Persistent (Frag n).
   Proof. by constructor. Qed.