diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 08d4ef1176a1577aede6a388b35e73f11f8be645..2944df3d03d3981e40ea0bb4eb03537473ec6306 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.