From c8dbb063cffe6275a75218d377c3174538396670 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 2 Jun 2019 10:27:56 +0200
Subject: [PATCH] Infinite docs: mention the generic constructions that should
 usually be used

---
 theories/base.v | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/theories/base.v b/theories/base.v
index 86d98c17..33ab00c9 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 := {}.
-- 
GitLab