diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index facbfd82b6b3528f68667dd184728e74ea1cc1c8..3c095092e3c1c9155c9eda102c04b5a43844a367 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -16,6 +16,9 @@ Class Dist A := dist : nat → relation A.
Instance: Params (@dist) 3.
Notation "x ≡{ n }≡ y" := (dist n x y)
(at level 70, n at next level, format "x ≡{ n }≡ y").
+Notation "x ≡{ n }@{ A }≡ y" := (dist (A:=A) n x y)
+ (at level 70, n at next level, only parsing).
+
Hint Extern 0 (_ ≡{_}≡ _) => reflexivity : core.
Hint Extern 0 (_ ≡{_}≡ _) => symmetry; assumption : core.
Notation NonExpansive f := (∀ n, Proper (dist n ==> dist n) f).