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

1 files changed, 5 insertions, 4 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.  *)