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

10 files changed, 34 insertions, 36 deletions

diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index b8301d0f4e..06ba2eb89b 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -1,3 +1,4 @@
+(* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v
index de05c296d2..30c08fdc12 100644
--- a/theories/ZArith/Int.v
+++ b/theories/ZArith/Int.v
@@ -6,14 +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$ *)
 
-(** An axiomatization of integers. *)
+(** * An light axiomatization of integers (used in FSetAVL). *)
 
 (** We define a signature for an integer datatype based on [Z].
     The goal is to allow a switch after extraction to ocaml's
diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v
index 51c2a2905a..36eb41104b 100644
--- a/theories/ZArith/Zabs.v
+++ b/theories/ZArith/Zabs.v
@@ -1,3 +1,4 @@
+(* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
diff --git a/theories/ZArith/Zbinary.v b/theories/ZArith/Zbinary.v
index 4c9ee24057..0a6c94986a 100644
--- a/theories/ZArith/Zbinary.v
+++ b/theories/ZArith/Zbinary.v
@@ -1,3 +1,4 @@
+(* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -16,27 +17,22 @@ Require Import ZArith.
 Require Export Zpower.
 Require Import Omega.
 
-(** L'évaluation des vecteurs de booléens se font à la fois en binaire et
-    en complément à  deux. Le nombre appartient à  Z.
-    On utilise donc Omega pour faire les calculs dans Z.
-    De plus, on utilise les fonctions 2^n où n est un naturel, ici la longueur.
-	two_power_nat = [n:nat](POS (shift_nat n xH))
-     		: nat->Z
-	two_power_nat_S
-	     : (n:nat)`(two_power_nat (S n)) = 2*(two_power_nat n)`
-	Z_lt_ge_dec
-	     : (x,y:Z){`x < y`}+{`x >= y`}
+(** The evaluation of boolean vector is done both in binary and
+    two's complement. The computed number belongs to Z.
+    We hence use Omega to perform computations in Z.
+    Moreover, we use functions [2^n] where [n] is a natural number
+    (here the vector length).
 *)
 
 
 Section VALUE_OF_BOOLEAN_VECTORS.
 
-(** Les calculs sont effectués dans la convention positive usuelle.
-    Les valeurs correspondent soit à  l'écriture binaire (nat),
-    soit au complément à  deux (int).
-    On effectue le calcul suivant le schéma de Horner.
-    Le complément à  deux n'a de sens que sur les vecteurs de taille
-    supérieure ou égale à  un, le bit de signe étant évalué négativement.
+(** Computations are done in the usual convention.
+    The values correspond either to the binary coding (nat) or
+    to the two's complement coding (int).
+    We perform the computation via Horner scheme.
+    The two's complement coding only makes sense on vectors whose
+    size is greater or equal to one (a sign bit should be present).
 *)
 
   Definition bit_value (b:bool) : Z :=
@@ -68,12 +64,12 @@ End VALUE_OF_BOOLEAN_VECTORS.
 
 Section ENCODING_VALUE.
 
-(** On calcule la valeur binaire selon un schema de Horner.
-    Le calcul s'arrete à  la longueur du vecteur sans vérification.
-    On definit une fonction Zmod2 calquee sur Zdiv2 mais donnant le quotient
-    de la division z=2q+r avec 0<=r<=1.
-    La valeur en complément à  deux est calculée selon un schema de Horner
-    avec Zmod2, le paramètre est la taille moins un.
+(** We compute the binary value via a Horner scheme.
+    Computation stops at the vector length without checks.
+    We define a function Zmod2 similar to Zdiv2 returning the
+    quotient of division z=2q+r with 0<=r<=1.
+    The two's complement value is also computed via a Horner scheme
+    with Zmod2, the parameter is the size minus one.
 *)
 
   Definition Zmod2 (z:Z) :=
@@ -134,9 +130,8 @@ End ENCODING_VALUE.
 
 Section Z_BRIC_A_BRAC.
 
-  (** Bibliotheque de lemmes utiles dans la section suivante.
-      Utilise largement ZArith.
-      Mériterait d'être récrite.
+  (** Some auxiliary lemmas used in the next section. Large use of ZArith.
+      Deserve to be properly rewritten.
   *)
 
   Lemma binary_value_Sn :
@@ -282,8 +277,8 @@ End Z_BRIC_A_BRAC.
 
 Section COHERENT_VALUE.
 
-(** On vérifie que dans l'intervalle de définition les fonctions sont
-    réciproques l'une de l'autre. Elles utilisent les lemmes du bric-a-brac.
+(** We check that the functions are reciprocal on the definition interval.
+    This uses earlier library lemmas.
 *)
 
   Lemma binary_to_Z_to_binary :
diff --git a/theories/ZArith/Zcompare.v b/theories/ZArith/Zcompare.v
index f146a80e13..2515b7f7b2 100644
--- a/theories/ZArith/Zcompare.v
+++ b/theories/ZArith/Zcompare.v
@@ -1,3 +1,4 @@
+(* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -9,7 +10,7 @@
 (*i $$ i*)
 
 (**********************************************************************)
-(** Binary Integers (Pierre Crégut, CNET, Lannion, France)            *)
+(** Binary Integers (Pierre Crégut, CNET, Lannion, France)            *)
 (**********************************************************************)
 
 Require Export BinPos.
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index 3435874cce..bc35ba4052 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -1,3 +1,4 @@
+(* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v
index c406a15426..dd35cd139f 100644
--- a/theories/ZArith/Zmin.v
+++ b/theories/ZArith/Zmin.v
@@ -1,3 +1,4 @@
+(* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v
index 46b23fe63c..3d9853ff09 100644
--- a/theories/ZArith/Znat.v
+++ b/theories/ZArith/Znat.v
@@ -1,3 +1,4 @@
+(* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v
index 7aef3ea8e8..70cbe0f28f 100644
--- a/theories/ZArith/Zorder.v
+++ b/theories/ZArith/Zorder.v
@@ -1,3 +1,4 @@
+(* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -7,7 +8,7 @@
 (************************************************************************)
 (*i $Id$ i*)
 
-(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *)
+(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
 
 Require Import BinPos.
 Require Import BinInt.
diff --git a/theories/ZArith/auxiliary.v b/theories/ZArith/auxiliary.v
index 6ebdcb50a9..7af99ece96 100644
--- a/theories/ZArith/auxiliary.v
+++ b/theories/ZArith/auxiliary.v
@@ -1,3 +1,4 @@
+(* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -8,7 +9,7 @@
 
 (*i $Id$ i*)
 
-(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
+(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
 
 Require Export Arith_base.
 Require Import BinInt.