Fix the stdlib doc compilation + switch all .v file to utf8

 1) compilation of Library.tex was failing on a "Ext_" in Diaconescu.v
    In fact coqdoc was trying to recognize the end of a _emphasis_ and
    hence inserted a bogus }. For the moment I've enclosed the phrase
    with [  ], but this emphasis "feature" of coqdoc seems _really_
    easy to broke. Matthieu ?

 2) By the way, this Library document was made from latin1 and utf8
    source file, hence bogus characters. All .v containing special
    characters are converted to utf8, and their first line is now
    mentionning this. (+ killed some old french comments and some
    other avoidable special characters).

  PLEASE: let's stick to this convention and avoid latin1, at least
    in .v files.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12363 85f007b7-540e-0410-9357-904b9bb8a0f7

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.