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, 17 insertions, 14 deletions

diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index 4b9b26384..e87482d84 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.v
@@ -6,11 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* Decidable equivalences.
- *
- * Author: Matthieu Sozeau
- * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
- *              91405 Orsay, France *)
+(** * Decidable equivalences.
+
+   Author: Matthieu Sozeau
+   Institution: LRI, CNRS UMR 8623 - University Paris Sud
+*)
 
 (* $Id$ *)
 
@@ -18,8 +18,8 @@
 
 Require Export Coq.Classes.Equivalence.
 
-(** The [DecidableSetoid] class asserts decidability of a [Setoid]. It can be useful in proofs to reason more
-   classically. *)
+(** The [DecidableSetoid] class asserts decidability of a [Setoid].
+   It can be useful in proofs to reason more classically. *)
 
 Require Import Coq.Logic.Decidable.
 Require Import Coq.Bool.Bool.
@@ -31,13 +31,15 @@ Open Scope equiv_scope.
 Class DecidableEquivalence `(equiv : Equivalence A) :=
   setoid_decidable : forall x y : A, decidable (x === y).
 
-(** The [EqDec] class gives a decision procedure for a particular setoid equality. *)
+(** The [EqDec] class gives a decision procedure for a particular
+   setoid equality. *)
 
 Class EqDec A R {equiv : Equivalence R} :=
   equiv_dec : forall x y : A, { x === y } + { x =/= y }.
 
-(** We define the [==] overloaded notation for deciding equality. It does not take precedence
-   of [==] defined in the type scope, hence we can have both at the same time. *)
+(** We define the [==] overloaded notation for deciding equality. It does not
+   take precedence of [==] defined in the type scope, hence we can have both
+   at the same time. *)
 
 Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70) : equiv_scope.
 
@@ -70,13 +72,14 @@ Infix "<>b" := nequiv_decb (no associativity, at level 70).
 
 (** Decidable leibniz equality instances. *)
 
-(** The equiv is burried inside the setoid, but we can recover it by specifying which setoid we're talking about. *)
+(** The equiv is burried inside the setoid, but we can recover it by specifying
+   which setoid we're talking about. *)
 
 Program Instance nat_eq_eqdec : EqDec nat eq := eq_nat_dec.
 
 Program Instance bool_eqdec : EqDec bool eq := bool_dec.
 
-Program Instance unit_eqdec : EqDec unit eq := λ x y, in_left.
+Program Instance unit_eqdec : EqDec unit eq := fun x y => in_left.
 
   Next Obligation.
   Proof.
@@ -105,8 +108,8 @@ Program Instance sum_eqdec `(EqDec A eq, EqDec B eq) :
       | inl _, inr _ | inr _, inl _ => in_right
     end }.
 
-(** Objects of function spaces with countable domains like bool have decidable equality.
-   Proving the reflection requires functional extensionality though. *)
+(** Objects of function spaces with countable domains like bool have decidable
+  equality. Proving the reflection requires functional extensionality though. *)
 
 Program Instance bool_function_eqdec `(EqDec A eq) : ! EqDec (bool -> A) eq :=
   { equiv_dec f g :=