diff --git a/CHANGELOG.md b/CHANGELOG.md
index 17fa7dac71a5c4b8d7d62859dfe059892feb02db..d7c576cc6518d45494e6dd530d1b5f3c840f20f1 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -33,6 +33,9 @@ Coq 8.11 is no longer supported in this version of Iris.
   algorithm.
 * Set `Hint Mode` for the classes `OfeDiscrete`, `Dist`, `Unit`, `CmraMorphism`,
   `rFunctorContractive`, `urFunctorContractive`.
+* Set `Hint Mode` for the stdpp class `Equiv`. This might require few spurious
+  type annotations until
+  [Coq bug #14441](https://github.com/coq/coq/issues/14441) is fixed.
 * Add `max_prefix_list` RA on lists whose composition is only defined when one
   operand is a prefix of the other. The result is the longer list.
 
diff --git a/iris/algebra/big_op.v b/iris/algebra/big_op.v
index 8d5d5e1eeae68fae10e3e051a277d8473bdb60dd..5bb45470789544c8150092f2b33f11965a016670 100644
--- a/iris/algebra/big_op.v
+++ b/iris/algebra/big_op.v
@@ -171,7 +171,8 @@ Section list.
     ([^o list] k ↦ y ∈ l1, f k y) ≡ ([^o list] k ↦ y ∈ l2, g k y).
   Proof.
     intros Hl Hf. apply big_opL_gen_proper_2; try (apply _ || done).
-    intros k. assert (l1 !! k ≡ l2 !! k) as Hlk by (by f_equiv).
+    (* FIXME (Coq #14441) unnecessary type annotation *)
+    intros k. assert (l1 !! k ≡@{option A} l2 !! k) as Hlk by (by f_equiv).
     destruct (l1 !! k) eqn:?, (l2 !! k) eqn:?; inversion Hlk; naive_solver.
   Qed.
 
@@ -324,7 +325,8 @@ Section gmap.
     ([^o map] k ↦ y ∈ m1, f k y) ≡ ([^o map] k ↦ y ∈ m2, g k y).
   Proof.
     intros Hl Hf. apply big_opM_gen_proper_2; try (apply _ || done).
-    intros k. assert (m1 !! k ≡ m2 !! k) as Hlk by (by f_equiv).
+    (* FIXME (Coq #14441) unnecessary type annotation *)
+    intros k. assert (m1 !! k ≡@{option A} m2 !! k) as Hlk by (by f_equiv).
     destruct (m1 !! k) eqn:?, (m2 !! k) eqn:?; inversion Hlk; naive_solver.
   Qed.
 
diff --git a/iris/prelude/prelude.v b/iris/prelude/prelude.v
index 936e9523e17ccf12af26e5eb15ba90e229d37f18..8c458361c768f9e0c7f926769bef73ed31f06d9b 100644
--- a/iris/prelude/prelude.v
+++ b/iris/prelude/prelude.v
@@ -7,3 +7,7 @@ Ltac done := stdpp.tactics.done.
 
 (** Iris itself and many dependencies still rely on this coercion. *)
 Coercion Z.of_nat : nat >-> Z.
+
+(* No Hint Mode set in stdpp because of Coq bugs #5735 and #9058, only
+fixed in Coq >= 8.12, which Iris depends on. *)
+Global Hint Mode Equiv ! : typeclass_instances.
diff --git a/tests/algebra.v b/tests/algebra.v
index c9f46319f46905926d47a6222184145a2d1afca1..39e569f17890255990a14ddfced501ef321cfa41 100644
--- a/tests/algebra.v
+++ b/tests/algebra.v
@@ -13,9 +13,6 @@ Section test_dist_equiv_mode.
   Lemma list_equiv_lookup_ofe {A : ofe} (l1 l2 : list A) :
     l1 ≡ l2 ↔ ∀ i, l1 !! i ≡ l2 !! i.
   Abort.
-  Lemma list_equiv_lookup_equiv `{Equiv A} (l1 l2 : list A) :
-    l1 ≡ l2 ↔ ∀ i, l1 !! i ≡ l2 !! i.
-  Abort.
 End test_dist_equiv_mode.
 
 (** Make sure that the same [Equivalence] instance is picked for Leibniz OFEs