From 6afa03321547a7bcf2ac6ce155ff368a3e1532fb Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 18 Mar 2020 18:49:27 +0100
Subject: [PATCH] make pair_core_id a new-unification-instance

---
 theories/algebra/cmra.v | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 08d4ef117..2944df3d0 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -1170,7 +1170,9 @@ Section prod.
     CmraDiscrete A â†’ CmraDiscrete B â†’ CmraDiscrete prodR.
   Proof. split. apply _. by intros ? []; split; apply cmra_discrete_valid. Qed.
 
-  Global Instance pair_core_id x y :
+  (* FIXME(Coq #6294): This is not an instance because we need it to use the new
+  unification. *)
+  Lemma pair_core_id x y :
     CoreId x â†’ CoreId y â†’ CoreId (x,y).
   Proof. by rewrite /CoreId prod_pcore_Some'. Qed.
 
@@ -1189,6 +1191,9 @@ Section prod.
   Proof. move=>? [??] [_ ?] [_ /=?]. eauto. Qed.
 End prod.
 
+(* Registering as [Hint Extern] with new unification. *)
+Hint Extern 4 (CoreId _) => notypeclasses refine (pair_core_id _ _ _ _) : typeclass_instances.
+
 Arguments prodR : clear implicits.
 
 Section prod_unit.
-- 
GitLab