diff --git a/CHANGELOG.md b/CHANGELOG.md
index bea7aca77135425a17d0aca4dc00c35e2557415d..569489fafb50c79a8f8b83b73a2d2bd51e64636d 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -31,7 +31,7 @@ Coq 8.11 is no longer supported in this version of Iris.
   `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.
-* Set `Hint Mode` for the classes `OfeDiscrete`, `Unit`, `CmraMorphism`,
+* Set `Hint Mode` for the classes `OfeDiscrete`, `Dist`, `Unit`, `CmraMorphism`,
   `rFunctorContractive`, `urFunctorContractive`.
 * 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/cmra.v b/iris/algebra/cmra.v
index 07f46ded4e3119ff2d9166cd72695e2ee8af4ef3..c8424ccff0b39347090aae9b372b7f9e0677dc9c 100644
--- a/iris/algebra/cmra.v
+++ b/iris/algebra/cmra.v
@@ -47,7 +47,7 @@ Section mixin.
     mixin_cmra_op_ne (x : A) : NonExpansive (op x);
     mixin_cmra_pcore_ne n (x y : A) cx :
       x ≡{n}≡ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≡{n}≡ cy;
-    mixin_cmra_validN_ne n : Proper (dist n ==> impl) (validN n);
+    mixin_cmra_validN_ne n : Proper (dist (A := A) n ==> impl) (validN n);
     (* valid *)
     mixin_cmra_valid_validN (x : A) : ✓ x ↔ ∀ n, ✓{n} x;
     mixin_cmra_validN_S n (x : A) : ✓{S n} x → ✓{n} x;
diff --git a/iris/algebra/gmap.v b/iris/algebra/gmap.v
index 55c589952bca7a858691b65aa8090ae5f7e9d351..3ea2bba6f2b23880a3dca1e11fb013ea6950e34d 100644
--- a/iris/algebra/gmap.v
+++ b/iris/algebra/gmap.v
@@ -66,7 +66,7 @@ Proof.
     [by constructor|by apply lookup_ne].
 Qed.
 Global Instance alter_ne (f : A → A) (k : K) n :
-  Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (alter f k).
+  Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (alter (M := gmap K A) f k).
 Proof. intros ? m m' Hm k'. by apply partial_alter_ne; [solve_proper|..]. Qed.
 
 Global Instance gmap_empty_discrete : Discrete (∅ : gmap K A).
diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index 96bf0991036e66514105910850125743182c6bfa..3fe741f8cbfd44e84733268303bb28492fbd84aa 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -13,6 +13,7 @@ Set Primitive Projections.
 
 (** Unbundled version *)
 Class Dist A := dist : nat → relation A.
+Global Hint Mode Dist ! : typeclass_instances.
 Global Instance: Params (@dist) 3 := {}.
 Notation "x ≡{ n }≡ y" := (dist n x y)
   (at level 70, n at next level, format "x  ≡{ n }≡  y").
diff --git a/tests/algebra.v b/tests/algebra.v
index ec82c57404bbb73cec3b2b50b39688da4dfe0ad2..5460faec3dd08b836e239201310574116c693121 100644
--- a/tests/algebra.v
+++ b/tests/algebra.v
@@ -1,6 +1,38 @@
 From iris.algebra Require Import auth excl lib.gmap_view.
 From iris.base_logic.lib Require Import invariants.
 
+Section test_dist_equiv_mode.
+  Local Unset Mangle Names.
+  (* check that the mode for [Dist] does not trigger https://github.com/coq/coq/issues/14441.
+  From https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/700#note_69303. *)
+
+  (* succeeds *)
+  Lemma list_dist_lookup {A : ofe} n (l1 l2 : list A) :
+    l1 ≡{n}≡ l2 ↔ ∀ i, l1 !! i ≡{n}≡ l2 !! i.
+  Abort.
+  (* analogous test for [Equiv] and https://github.com/coq/coq/issues/14441.
+  From https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/700#note_69303. *)
+
+  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.
+
+  Local Hint Mode Equiv ! : typeclass_instances.
+
+  (* succeeds *)
+  Lemma list_equiv_lookup_ofe {A : ofe} (l1 l2 : list A) :
+    l1 ≡ l2 ↔ ∀ i, l1 !! i ≡ l2 !! i.
+  Abort.
+
+  (* fails due to https://github.com/coq/coq/issues/14441; commented out, hoping
+  for a fix in Coq. *)
+  (* Fail Lemma list_equiv_lookup_equiv `{Equiv A} (l1 l2 : list A) :
+    l1 ≡ l2 ↔ ∀ i, l1 !! i ≡ l2 !! i. *)
+End test_dist_equiv_mode.
+
 (** 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 *)