diff --git a/theories/base.v b/theories/base.v
index 86d98c17b6e8d2ac44d9ab595aeebbb89637c321..33ab00c95697d0b31bf79b55177f34673d59b493 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -1226,7 +1226,10 @@ to pick fresh elements from other data structure like sets. See the file
 [FinSet C A].
 
 Note: we require [fresh] to respect permutations, which is needed to define the
-aforementioned [fresh] function on finite sets that respects set equality. *)
+aforementioned [fresh] function on finite sets that respects set equality.
+
+Instead of instantiating [Infinite] directly, consider using [max_infinite] or
+[inj_infinite] from the [infinite] module. *)
 Class Fresh A C := fresh: C → A.
 Hint Mode Fresh - ! : typeclass_instances.
 Instance: Params (@fresh) 3 := {}.