From f2eabe78463a0ad065ce4ebbd7da71531b60ef32 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 12 Mar 2020 21:48:32 +0100
Subject: [PATCH] Close issue #299: `leibnizO` finds convoluted proof for
 definitions

---
 tests/algebra.v        | 8 ++++++++
 theories/algebra/ofe.v | 5 ++++-
 2 files changed, 12 insertions(+), 1 deletion(-)

diff --git a/tests/algebra.v b/tests/algebra.v
index b744b8650..92c42c4b4 100644
--- a/tests/algebra.v
+++ b/tests/algebra.v
@@ -1,5 +1,13 @@
 From iris.base_logic.lib Require Import invariants.
 
+(** Make sure that the same [Equivalence] instance is picked for Leibniz OFEs
+with carriers that are definitionally equal. See also
+https://gitlab.mpi-sws.org/iris/iris/issues/299 *)
+Definition tag := nat.
+Canonical Structure tagO := leibnizO tag.
+Goal tagO = natO.
+Proof. reflexivity. Qed.
+
 Instance test_cofe {Σ} : Cofe (iPrePropO Σ) := _.
 
 Section tests.
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 1454393e0..ad309364b 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -885,7 +885,10 @@ Section discrete_ofe.
 End discrete_ofe.
 
 Notation discreteO A := (OfeT A (discrete_ofe_mixin _)).
-Notation leibnizO A := (OfeT A (@discrete_ofe_mixin _ equivL _)).
+(** Force the [Equivalence] proof to be [eq_equivalence] so that it does not
+find another one, like [ofe_equivalence], in the case of aliases. See also
+https://gitlab.mpi-sws.org/iris/iris/issues/229 *)
+Notation leibnizO A := (OfeT A (@discrete_ofe_mixin _ equivL eq_equivalence)).
 
 (** 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
-- 
GitLab