diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 6400459780ec5b8dff0a327426f694bbf4b62d2e..c54e539c377bb13a6656fdf7e242e11a3e3e25f5 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -38,9 +38,9 @@ Tactic Notation "ofe_subst" :=
   end.
 
 Record OfeMixin A `{Equiv A, Dist A} := {
-  mixin_equiv_dist x y : x ≡ y ↔ ∀ n, x ≡{n}≡ y;
-  mixin_dist_equivalence n : Equivalence (dist n);
-  mixin_dist_S n x y : x ≡{S n}≡ y → x ≡{n}≡ y
+  mixin_equiv_dist (x y : A) : x ≡ y ↔ ∀ n, x ≡{n}≡ y;
+  mixin_dist_equivalence n : Equivalence (@dist A _ n);
+  mixin_dist_S n (x y : A) : x ≡{S n}≡ y → x ≡{n}≡ y
 }.
 
 (** Bundled version *)