diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3322b97f55cbedb5ba7cec84c267f7ec059f1b23..923b66e6f42ef476f01d425dda95bd43eecc2ff6 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -27,6 +27,10 @@ Coq 8.11 is no longer supported in this version of Iris.
 * Demote the Camera structure on `list` to `iris_staging` since its composition
   is not very well-behaved.
 * Extend `gmap_view` with lemmas for "big" operations on maps.
+* Typeclasses instances triggering a canonical structure search such as `Equiv`,
+  `Dist`, `Op`, `Valid`, `ValidN`, `Unit`, `PCore` now use an `Hint Extern`
+  based on `refine` instead of `apply`, in order to use Coq's newer unification
+  algorithm.
 
 **Changes in `bi`:**
 
diff --git a/iris/algebra/cmra.v b/iris/algebra/cmra.v
index 43a8a068c5b930af446bf568119716af392e9831..7824e3ac84e51dddbe0d5ba12a73241b8260741e 100644
--- a/iris/algebra/cmra.v
+++ b/iris/algebra/cmra.v
@@ -93,10 +93,11 @@ Global Arguments cmra_validN : simpl never.
 Global Arguments cmra_ofe_mixin : simpl never.
 Global Arguments cmra_mixin : simpl never.
 Add Printing Constructor cmra.
-Global Hint Extern 0 (PCore _) => eapply (@cmra_pcore _) : typeclass_instances.
-Global Hint Extern 0 (Op _) => eapply (@cmra_op _) : typeclass_instances.
-Global Hint Extern 0 (Valid _) => eapply (@cmra_valid _) : typeclass_instances.
-Global Hint Extern 0 (ValidN _) => eapply (@cmra_validN _) : typeclass_instances.
+(* FIXME(Coq #6294) : we need the new unification algorithm here. *)
+Global Hint Extern 0 (PCore _) => refine (cmra_pcore _); shelve : typeclass_instances.
+Global Hint Extern 0 (Op _) => refine (cmra_op _); shelve : typeclass_instances.
+Global Hint Extern 0 (Valid _) => refine (cmra_valid _); shelve : typeclass_instances.
+Global Hint Extern 0 (ValidN _) => refine (cmra_validN _); shelve : typeclass_instances.
 Coercion cmra_ofeO (A : cmra) : ofe := Ofe A (cmra_ofe_mixin A).
 Canonical Structure cmra_ofeO.
 
@@ -215,7 +216,8 @@ Global Arguments ucmra_ofe_mixin : simpl never.
 Global Arguments ucmra_cmra_mixin : simpl never.
 Global Arguments ucmra_mixin : simpl never.
 Add Printing Constructor ucmra.
-Global Hint Extern 0 (Unit _) => eapply (@ucmra_unit _) : typeclass_instances.
+(* FIXME(Coq #6294) : we need the new unification algorithm here. *)
+Global Hint Extern 0 (Unit _) => refine (ucmra_unit _); shelve : typeclass_instances.
 Coercion ucmra_ofeO (A : ucmra) : ofe := Ofe A (ucmra_ofe_mixin A).
 Canonical Structure ucmra_ofeO.
 Coercion ucmra_cmraR (A : ucmra) : cmra :=
@@ -1543,7 +1545,7 @@ Section option_prod.
   Proof. intros ?%Some_pair_included. by rewrite -(Some_included_total b1). Qed.
 End option_prod.
 
-Lemma option_fmap_mono {A B : cmra} (f : A → B) ma mb :
+Lemma option_fmap_mono {A B : cmra} (f : A → B) (ma mb : option A) :
   Proper ((≡) ==> (≡)) f →
   (∀ a b, a ≼ b → f a ≼ f b) →
   ma ≼ mb → f <$> ma ≼ f <$> mb.
diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index 68c57a3f3cd01e38e9b5fbe14e57ff339e3e6367..65dab9152f935aa475f266b435956908ccf95e77 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -56,8 +56,9 @@ Structure ofe := Ofe {
 }.
 Global Arguments Ofe _ {_ _} _.
 Add Printing Constructor ofe.
-Global Hint Extern 0 (Equiv _) => eapply (@ofe_equiv _) : typeclass_instances.
-Global Hint Extern 0 (Dist _) => eapply (@ofe_dist _) : typeclass_instances.
+(* FIXME(Coq #6294) : we need the new unification algorithm here. *)
+Global Hint Extern 0 (Equiv _) => refine (ofe_equiv _); shelve : typeclass_instances.
+Global Hint Extern 0 (Dist _) => refine (ofe_dist _); shelve : typeclass_instances.
 Global Arguments ofe_car : simpl never.
 Global Arguments ofe_equiv : simpl never.
 Global Arguments ofe_dist : simpl never.