8 files changed, 10 insertions, 43 deletions
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index 189cf88ad2..a53a485d37 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -1,4 +1,3 @@
-
 (***********************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
 (* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v
index 52766bf967..c4b8f2a8d9 100644
--- a/theories/FSets/FMapFullAVL.v
+++ b/theories/FSets/FMapFullAVL.v
@@ -1,4 +1,3 @@
-
 (***********************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
 (* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index 112ccce30a..da5b358744 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -6,13 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* Finite sets library.
- * Authors: Pierre Letouzey and Jean-Christophe Filliâtre
- * Institution: LRI, CNRS UMR 8623 - Université Paris Sud
- *              91405 Orsay, France *)
-
 (* $Id$ *)
 
+(** * FMapPositive : an implementation of FMapInterface for [positive] keys. *)
+
 Require Import Bool.
 Require Import ZArith.
 Require Import OrderedType.
@@ -20,17 +17,14 @@ Require Import OrderedTypeEx.
 Require Import FMapInterface.
 
 Set Implicit Arguments.
-
 Open Local Scope positive_scope.
 
-(** * An implementation of [FMapInterface.S] for positive keys. *)
-
 (** This file is an adaptation to the [FMap] framework of a work by
   Xavier Leroy and Sandrine Blazy (used for building certified compilers).
   Keys are of type [positive], and maps are binary trees: the sequence
   of binary digits of a positive number corresponds to a path in such a tree.
-  This is quite similar to the [IntMap] library, except that no path compression
-  is implemented, and that the current file is simple enough to be
+  This is quite similar to the [IntMap] library, except that no path
+  compression is implemented, and that the current file is simple enough to be
   self-contained. *)
 
 (** Even if [positive] can be seen as an ordered type with respect to the
diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v
index 0f0e675ee7..36964ad01a 100644
--- a/theories/FSets/FSetAVL.v
+++ b/theories/FSets/FSetAVL.v
@@ -1,3 +1,4 @@
+(* -*- coding: utf-8 -*- *)
 (***********************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
 (* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
@@ -6,16 +7,11 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* Finite sets library.
- * Authors: Pierre Letouzey and Jean-Christophe Filliâtre
- * Institution: LRI, CNRS UMR 8623 - Université Paris Sud
- *              91405 Orsay, France *)
-
 (* $Id$ *)
 
-(** * FSetAVL *)
+(** * FSetAVL : Implementation of FSetInterface via AVL trees *)
 
-(** This module implements sets using AVL trees.
+(** This module implements finite sets using AVL trees.
     It follows the implementation from Ocaml's standard library,
 
     All operations given here expect and produce well-balanced trees
diff --git a/theories/FSets/FSetFullAVL.v b/theories/FSets/FSetFullAVL.v
index bc0d758bd8..d8a31ba5f7 100644
--- a/theories/FSets/FSetFullAVL.v
+++ b/theories/FSets/FSetFullAVL.v
@@ -6,16 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* Finite sets library.
- * Authors: Pierre Letouzey and Jean-Christophe Filliâtre
- * Institution: LRI, CNRS UMR 8623 - Université Paris Sud
- *              91405 Orsay, France *)
-
 (* $Id$ *)
 
-(** * FSetFullAVL
-
-   This file contains some complements to [FSetAVL].
+(** * FSetFullAVL : some complements to FSetAVL
 
    - Functor [AvlProofs] proves that trees of [FSetAVL] are not only
    binary search trees, but moreover well-balanced ones. This is done
diff --git a/theories/FSets/FSetToFiniteSet.v b/theories/FSets/FSetToFiniteSet.v
index 23420109cb..01138270e2 100644
--- a/theories/FSets/FSetToFiniteSet.v
+++ b/theories/FSets/FSetToFiniteSet.v
@@ -6,13 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* Finite sets library.
- * Authors: Pierre Letouzey and Jean-Christophe Filliâtre
- * Institution: LRI, CNRS UMR 8623 - Université Paris Sud
- *              91405 Orsay, France *)
-
 (* $Id$ *)
 
+(** * Finite sets library : conversion to old [Finite_sets] *)
+
 Require Import Ensembles Finite_sets.
 Require Import FSetInterface FSetProperties OrderedTypeEx DecidableTypeEx.
 
diff --git a/theories/FSets/OrderedTypeAlt.v b/theories/FSets/OrderedTypeAlt.v
index 3a9fa1a734..23ae4c85a3 100644
--- a/theories/FSets/OrderedTypeAlt.v
+++ b/theories/FSets/OrderedTypeAlt.v
@@ -5,12 +5,6 @@
 (*    //   *      This file is distributed under the terms of the      *)
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
-
-(* Finite sets library.
- * Authors: Pierre Letouzey and Jean-Christophe Filliâtre
- * Institution: LRI, CNRS UMR 8623 - Université Paris Sud
- *              91405 Orsay, France *)
-
 (* $Id$ *)
 
 Require Import OrderedType.
diff --git a/theories/FSets/OrderedTypeEx.v b/theories/FSets/OrderedTypeEx.v
index e76cead2dd..a39f336a57 100644
--- a/theories/FSets/OrderedTypeEx.v
+++ b/theories/FSets/OrderedTypeEx.v
@@ -6,11 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* Finite sets library.
- * Authors: Pierre Letouzey and Jean-Christophe Filliâtre
- * Institution: LRI, CNRS UMR 8623 - Université Paris Sud
- *              91405 Orsay, France *)
-
 (* $Id$ *)
 
 Require Import OrderedType.