From 30a9a27ce3a76e2704671174483d4b4f84c482e4 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 17 Nov 2014 17:06:21 +0100
Subject: Clarifying the role of ListSet.v in the library, compared to other
 finite set libraries.

---
 theories/Lists/ListSet.v | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v
index f02c1d13f8..908731117c 100644
--- a/theories/Lists/ListSet.v
+++ b/theories/Lists/ListSet.v
@@ -6,11 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** A Library for finite sets, implemented as lists *)
+(** A library for finite sets, implemented as lists *)
 
-(** List is loaded, but not exported.
-    This allow to "hide" the definitions, functions and theorems of List
-    and to see only the ones of ListSet *)
+(** This is a light implementation of finite sets as lists; for a more
+    extensive library, you might rather consider MSetWeakList.v. In
+    addition, if your domain is totally ordered, you might also
+    consider implementations of finite sets with access in logarithmic
+    time (e.g. MSetRBT.v which is based on red-black trees). *)
 
 Require Import List.
 
-- 
cgit v1.2.3