diff --git a/CHANGELOG.md b/CHANGELOG.md
index 607fdf3d9218bbec8a0d23bd0c8950d49eb250c8..86a90e1005d30d3d9cc12867df8995d477818380 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`.
 
 **Changes in `bi`:**
diff --git a/iris/algebra/cmra.v b/iris/algebra/cmra.v
index 5dde79ec0062a1db155c08bc5836e40071a0b7a5..6f73d5d547251893479f7e6a22e4e098dd489c09 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 a61482362eb7dc35455ed4883b7ec8fd4703e30c..274a3020e2b545806ab12c9262eb282b7a072a33 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").