diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 1bf21d0e0708e5d6a4611db3b45385dbd43b8190..9f513eea967dbd0b3d35f2182eedab521de306be 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -1073,7 +1073,8 @@ Qed.
 
 (** Sigma *)
 Class LimitPreserving `{!Cofe A} (P : A → Prop) : Prop :=
-  limit_preserving : ∀ c : chain A, (∀ n, P (c n)) → P (compl c).
+  limit_preserving (c : chain A) : (∀ n, P (c n)) → P (compl c).
+Hint Mode LimitPreserving + + ! : typeclass_instances.
 
 Section limit_preserving.
   Context {A : ofeT} `{!Cofe A}.