1 files changed, 12 insertions, 10 deletions
diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v
index 37d051a3..0a0bf0de 100644
--- a/theories/Lists/ListSet.v
+++ b/theories/Lists/ListSet.v
@@ -1,16 +1,18 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       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.
 
@@ -116,7 +118,7 @@ Section first_definitions.
     simple induction x; simpl; intros.
     apply H0; red; trivial.
     case (Aeq_dec a a0); auto with datatypes.
-    intro; apply H; intros; auto.
+    intro Hneg; apply H; intros; auto.
     apply H1; red; intro.
     case H3; auto.
   Qed.
@@ -147,8 +149,8 @@ Section first_definitions.
     simple induction x; simpl.
     tauto.
     intros a0 l; elim (Aeq_dec a a0).
-    intros; discriminate H0.
-    unfold not; intros; elim H1; auto with datatypes.
+    intros _ _ [=].
+    unfold not; intros H H0 H1 [|]; auto with datatypes.
   Qed.
 
   Lemma set_mem_complete2 :
@@ -157,7 +159,7 @@ Section first_definitions.
     simple induction x; simpl.
     tauto.
     intros a0 l; elim (Aeq_dec a a0).
-    intros; elim H0; auto with datatypes.
+    intros H H0 []; auto with datatypes.
     tauto.
   Qed.
 
@@ -204,7 +206,7 @@ Section first_definitions.
     simpl; do 3 intro.
     elim (Aeq_dec b a0).
     simpl; tauto.
-    simpl; intros; elim H0.
+    simpl; intros H0 [|].
     trivial with datatypes.
     tauto.
     tauto.