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, 24 insertions, 18 deletions

diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index 32880b2f7..02e6d3daf 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.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 *)
@@ -81,7 +82,7 @@ unpublished.
 [[Bell93]] John L. Bell, Hilbert's Epsilon Operator in Intuitionistic
 Type Theories, Mathematical Logic Quarterly, volume 39, 1993.
 
-[Carlstrøm05] Jesper Carlstrøm, Interpreting descriptions in
+[Carlström05] Jesper Carlström, Interpreting descriptions in
 intentional type theory, Journal of Symbolic Logic 70(2):488-514, 2005.
 *)
 
@@ -126,7 +127,7 @@ Definition FunctionalRelReification_on :=
 
 (** ID_epsilon (constructive version of indefinite description;
     combined with proof-irrelevance, it may be connected to
-    Carlstrøm's type theory with a constructive indefinite description
+    Carlström's type theory with a constructive indefinite description
     operator) *)
 
 Definition ConstructiveIndefiniteDescription_on :=
@@ -134,7 +135,7 @@ Definition ConstructiveIndefiniteDescription_on :=
     (exists x, P x) -> { x:A | P x }.
 
 (** ID_iota (constructive version of definite description; combined
-    with proof-irrelevance, it may be connected to Carlstrøm's and
+    with proof-irrelevance, it may be connected to Carlström's and
     Stenlund's type theory with a constructive definite description
     operator) *)
 
@@ -764,7 +765,7 @@ be applied on the same Type universes on both sides of the first
     We adapt the proof to show that constructive definite description
     transports excluded-middle from [Prop] to [Set].
 
-    [[ChicliPottierSimpson02]] Laurent Chicli, Loïc Pottier, Carlos
+    [[ChicliPottierSimpson02]] Laurent Chicli, Loïc Pottier, Carlos
     Simpson, Mathematical Quotients and Quotient Types in Coq,
     Proceedings of TYPES 2002, Lecture Notes in Computer Science 2646,
     Springer Verlag.  *)
diff --git a/theories/Logic/ClassicalEpsilon.v b/theories/Logic/ClassicalEpsilon.v
index 0d65a89ba..cee55dc81 100644
--- a/theories/Logic/ClassicalEpsilon.v
+++ b/theories/Logic/ClassicalEpsilon.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 *)
@@ -74,7 +75,7 @@ Definition epsilon_spec (A : Type) (i:inhabited A) (P : A->Prop) :
 
 (** A proof that if [P] is inhabited, [epsilon a P] does not depend on
     the actual proof that the domain of [P] is inhabited
-    (proof idea kindly provided by Pierre Castéran) *)
+    (proof idea kindly provided by Pierre Castéran) *)
 
 Lemma epsilon_inh_irrelevance :
    forall (A:Type) (i j : inhabited A) (P:A->Prop),
diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v
index 9ec916a7d..b22a3a874 100644
--- a/theories/Logic/ClassicalFacts.v
+++ b/theories/Logic/ClassicalFacts.v
@@ -31,7 +31,7 @@ Table of contents:
 
 3.1. Weak excluded middle
 
-3.2. Gödel-Dummett axiom and right distributivity of implication over
+3.2. Gödel-Dummett axiom and right distributivity of implication over
      disjunction
 
 3 3. Independence of general premises and drinker's paradox
@@ -290,7 +290,7 @@ End Proof_irrelevance_CIC.
   cannot be refined.
 
   [[Berardi90]] Stefano Berardi, "Type dependence and constructive
-  mathematics", Ph. D. thesis, Dipartimento Matematica, Università di
+  mathematics", Ph. D. thesis, Dipartimento Matematica, Università di
   Torino, 1990.
 *)
 
@@ -417,7 +417,7 @@ End Proof_irrelevance_CCI.
 
 (** We show the following increasing in the strength of axioms:
  - weak excluded-middle
- - right distributivity of implication over disjunction and Gödel-Dummett axiom
+ - right distributivity of implication over disjunction and Gödel-Dummett axiom
  - independence of general premises and drinker's paradox
  - excluded-middle
 *)
@@ -436,20 +436,20 @@ Definition weak_excluded_middle :=
 
 (** The interest in the equivalent variant
     [weak_generalized_excluded_middle] is that it holds even in logic
-    without a primitive [False] connective (like Gödel-Dummett axiom) *)
+    without a primitive [False] connective (like Gödel-Dummett axiom) *)
 
 Definition weak_generalized_excluded_middle :=
   forall A B:Prop, ((A -> B) -> B) \/ (A -> B).
 
-(** ** Gödel-Dummett axiom *)
+(** ** Gödel-Dummett axiom *)
 
-(** [(A->B) \/ (B->A)] is studied in [[Dummett59]] and is based on [[Gödel33]].
+(** [(A->B) \/ (B->A)] is studied in [[Dummett59]] and is based on [[Gödel33]].
 
     [[Dummett59]] Michael A. E. Dummett. "A Propositional Calculus
     with a Denumerable Matrix", In the Journal of Symbolic Logic, Vol
     24 No. 2(1959), pp 97-103.
 
-    [[Gödel33]] Kurt Gödel. "Zum intuitionistischen Aussagenkalkül",
+    [[Gödel33]] Kurt Gödel. "Zum intuitionistischen Aussagenkalkül",
     Ergeb. Math. Koll. 4 (1933), pp. 34-38.
  *)
 
@@ -500,13 +500,13 @@ Qed.
 
     It is a generalization to predicate logic of the right
     distributivity of implication over disjunction (hence of
-    Gödel-Dummett axiom) whose own constructive form (obtained by a
+    Gödel-Dummett axiom) whose own constructive form (obtained by a
     restricting the third formula to be negative) is called
     Kreisel-Putnam principle [[KreiselPutnam57]].
 
     [[KreiselPutnam57]], Georg Kreisel and Hilary Putnam. "Eine
-    Unableitsbarkeitsbeweismethode für den intuitionistischen
-    Aussagenkalkül". Archiv für Mathematische Logik und
+    Unableitsbarkeitsbeweismethode für den intuitionistischen
+    Aussagenkalkül". Archiv für Mathematische Logik und
     Graundlagenforschung, 3:74- 78, 1957.
 
     [[Troelstra73]], Anne Troelstra, editor. Metamathematical
diff --git a/theories/Logic/ClassicalUniqueChoice.v b/theories/Logic/ClassicalUniqueChoice.v
index c1f9881fa..2a32323cb 100644
--- a/theories/Logic/ClassicalUniqueChoice.v
+++ b/theories/Logic/ClassicalUniqueChoice.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 *)
@@ -19,7 +20,7 @@
     excluded-middle in [Set], hence it implies a strongly classical
     world. Especially it conflicts with the impredicativity of [Set].
 
-    [ChicliPottierSimpson02] Laurent Chicli, Loïc Pottier, Carlos
+    [ChicliPottierSimpson02] Laurent Chicli, Loïc Pottier, Carlos
     Simpson, Mathematical Quotients and Quotient Types in Coq,
     Proceedings of TYPES 2002, Lecture Notes in Computer Science 2646,
     Springer Verlag.  *)
diff --git a/theories/Logic/ConstructiveEpsilon.v b/theories/Logic/ConstructiveEpsilon.v
index 337ee05b6..6d22b1a9e 100644
--- a/theories/Logic/ConstructiveEpsilon.v
+++ b/theories/Logic/ConstructiveEpsilon.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/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v
index 18f3181b6..22c838c26 100644
--- a/theories/Logic/Diaconescu.v
+++ b/theories/Logic/Diaconescu.v
@@ -39,7 +39,7 @@
    [Bell93] John L. Bell, Hilbert's epsilon operator and classical
    logic, Journal of Philosophical Logic, 22: 1-18, 1993
 
-   [Carlström04] Jesper Carlström, EM + Ext_ + AC_int <-> AC_ext,
+   [Carlström04] Jesper Carlström, [EM + Ext_ + AC_int <-> AC_ext],
    Mathematical Logic Quaterly, vol 50(3), pp 236-240, 2004.
 *)
 
diff --git a/theories/Logic/Eqdep.v b/theories/Logic/Eqdep.v
index 3c3b7bbfa..5c6b4e89f 100644
--- a/theories/Logic/Eqdep.v
+++ b/theories/Logic/Eqdep.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/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v
index a4b4b5b4a..4689fb46c 100644
--- a/theories/Logic/EqdepFacts.v
+++ b/theories/Logic/EqdepFacts.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 *)
@@ -25,7 +26,7 @@
   References:
 
   [1] T. Streicher, Semantical Investigations into Intensional Type Theory,
-      Habilitationsschrift, LMU München, 1993.
+      Habilitationsschrift, LMU München, 1993.
   [2] M. Hofmann, T. Streicher, The groupoid interpretation of type theory,
       Proceedings of the meeting Twenty-five years of constructive
       type theory, Venice, Oxford University Press, 1998