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

12 files changed, 91 insertions, 77 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 :=
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index aa20ebd49..78e66d374 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -6,11 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* Typeclass-based setoids. Definitions on [Equivalence].
+(** * Typeclass-based setoids. Definitions on [Equivalence].
 
    Author: Matthieu Sozeau
-   Institution: LRI, CNRS UMR 8623 - Universit�copyright Paris Sud
-   91405 Orsay, France *)
+   Institution: LRI, CNRS UMR 8623 - University Paris Sud
+*)
 
 (* $Id$ *)
 
@@ -29,7 +29,8 @@ Open Local Scope signature_scope.
 
 Definition equiv `{Equivalence A R} : relation A := R.
 
-(** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *)
+(** Overloaded notations for setoid equivalence and inequivalence.
+    Not to be confused with [eq] and [=]. *)
 
 Notation " x === y " := (equiv x y) (at level 70, no associativity) : equiv_scope.
 
diff --git a/theories/Classes/Functions.v b/theories/Classes/Functions.v
index 80d60d658..8c6161036 100644
--- a/theories/Classes/Functions.v
+++ b/theories/Classes/Functions.v
@@ -6,11 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* Functional morphisms.
+(** * Functional morphisms.
 
    Author: Matthieu Sozeau
-   Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
-   91405 Orsay, France *)
+   Institution: LRI, CNRS UMR 8623 - University Paris Sud
+*)
 
 (* $Id$ *)
 
diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v
index 7be92139e..f6e51018a 100644
--- a/theories/Classes/Init.v
+++ b/theories/Classes/Init.v
@@ -6,12 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* Initialization code for typeclasses, setting up the default tactic
+(** * Initialization code for typeclasses, setting up the default tactic
    for instance search.
 
    Author: Matthieu Sozeau
-   Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
-   91405 Orsay, France *)
+   Institution: LRI, CNRS UMR 8623 - University Paris Sud
+*)
 
 (* $Id$ *)
 
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 55aad6e73..656b9d74e 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-name: "~/research/coq/trunk/bin/coqtop.byte"; coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.Morphisms"); compile-command: "make -C ../.. TIME='time -p'" -*- *)
+(* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -7,11 +7,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* Typeclass-based morphism definition and standard, minimal instances.
+(** * Typeclass-based morphism definition and standard, minimal instances
 
    Author: Matthieu Sozeau
-   Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
-   91405 Orsay, France *)
+   Institution: LRI, CNRS UMR 8623 - University Paris Sud
+*)
 
 (* $Id$ *)
 
@@ -26,8 +26,8 @@ Require Export Coq.Classes.RelationClasses.
    These will be used by the [setoid_rewrite] tactic later. *)
 
 (** A morphism for a relation [R] is a proper element of the relation.
-   The relation [R] will be instantiated by [respectful] and [A] by an arrow type
-   for usual morphisms. *)
+   The relation [R] will be instantiated by [respectful] and [A] by an arrow
+   type for usual morphisms. *)
 
 Class Proper {A} (R : relation A) (m : A) : Prop :=
   proper : R m m.
diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v
index 5b61e2c07..dbe7b5c88 100644
--- a/theories/Classes/Morphisms_Prop.v
+++ b/theories/Classes/Morphisms_Prop.v
@@ -6,11 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* [Proper] instances for propositional connectives.
+(** * [Proper] instances for propositional connectives.
 
    Author: Matthieu Sozeau
-   Institution: LRI, CNRS UMR 8623 - Université Paris Sud
-   91405 Orsay, France *)
+   Institution: LRI, CNRS UMR 8623 - University Paris Sud
+*)
 
 Require Import Coq.Classes.Morphisms.
 Require Import Coq.Program.Basics.
@@ -56,11 +56,11 @@ Program Instance ex_iff_morphism {A : Type} : Proper (pointwise_relation A iff =
   Proof.
     unfold pointwise_relation in H.
     split ; intros.
-    destruct H0 as [x₁ H₁].
-    exists x₁. rewrite H in H₁. assumption.
+    destruct H0 as [x1 H1].
+    exists x1. rewrite H in H1. assumption.
 
-    destruct H0 as [x₁ H₁].
-    exists x₁. rewrite H. assumption.
+    destruct H0 as [x1 H1].
+    exists x1. rewrite H. assumption.
   Qed.
 
 Program Instance ex_impl_morphism {A : Type} :
diff --git a/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v
index e9301298e..9c42ff155 100644
--- a/theories/Classes/Morphisms_Relations.v
+++ b/theories/Classes/Morphisms_Relations.v
@@ -6,11 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* Morphism instances for relations.
+(** * Morphism instances for relations.
 
    Author: Matthieu Sozeau
-   Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
-   91405 Orsay, France *)
+   Institution: LRI, CNRS UMR 8623 - University Paris Sud
+*)
 
 Require Import Relation_Definitions.
 Require Import Coq.Classes.Morphisms.
@@ -38,8 +38,8 @@ Lemma predicate_implication_pointwise (l : list Type) :
   Proper (@predicate_implication l ==> pointwise_lifting impl l) id.
 Proof. do 2 red. unfold predicate_implication. auto. Qed.
 
-(** The instanciation at relation allows to rewrite applications of relations [R x y] to [R' x y] *)
-(*    when [R] and [R'] are in [relation_equivalence]. *)
+(** The instanciation at relation allows to rewrite applications of relations
+    [R x y] to [R' x y]  when [R] and [R'] are in [relation_equivalence]. *)
 
 Instance relation_equivalence_pointwise :
   Proper (relation_equivalence ==> pointwise_relation A (pointwise_relation A iff)) id.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index b2f62cb87..0222ad115 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.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 *)
@@ -6,12 +7,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* Typeclass-based relations, tactics and standard instances.
+(** *  Typeclass-based relations, tactics and standard instances
+
    This is the basic theory needed to formalize morphisms and setoids.
 
    Author: Matthieu Sozeau
-   Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
-   91405 Orsay, France *)
+   Institution: LRI, CNRS UMR 8623 - University Paris Sud
+*)
 
 (* $Id$ *)
 
diff --git a/theories/Classes/SetoidAxioms.v b/theories/Classes/SetoidAxioms.v
index ebc1d7be9..ef115b2ed 100644
--- a/theories/Classes/SetoidAxioms.v
+++ b/theories/Classes/SetoidAxioms.v
@@ -6,11 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* Extensionality axioms that can be used when reasoning with setoids.
- *
- * Author: Matthieu Sozeau
- * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
- *              91405 Orsay, France *)
+(** * Extensionality axioms that can be used when reasoning with setoids.
+
+   Author: Matthieu Sozeau
+   Institution: LRI, CNRS UMR 8623 - University Paris Sud
+*)
 
 (* $Id$ *)
 
@@ -21,7 +21,7 @@ Unset Strict Implicit.
 
 Require Export Coq.Classes.SetoidClass.
 
-(* Application of the extensionality axiom to turn a goal on
+(** Application of the extensionality axiom to turn a goal on
    Leibniz equality to a setoid equivalence (use with care!). *)
 
 Axiom setoideq_eq : forall `{sa : Setoid a} (x y : a), x == y -> x = y.
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index 6af4b5ffe..33d98548d 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -6,11 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* Typeclass-based setoids, tactics and standard instances.
+(** * Typeclass-based setoids, tactics and standard instances.
 
    Author: Matthieu Sozeau
-   Institution: LRI, CNRS UMR 8623 - Universit�copyright Paris Sud
-   91405 Orsay, France *)
+   Institution: LRI, CNRS UMR 8623 - University Paris Sud
+*)
 
 (* $Id$ *)
 
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index 71d80c959..32e75adae 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.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 *)
@@ -6,11 +7,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* Decidable setoid equality theory.
- *
- * Author: Matthieu Sozeau
- * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
- *              91405 Orsay, France *)
+(** * Decidable setoid equality theory.
+
+   Author: Matthieu Sozeau
+   Institution: LRI, CNRS UMR 8623 - University Paris Sud
+*)
 
 (* $Id$ *)
 
@@ -21,21 +22,23 @@ Unset Strict Implicit.
 
 Require Export Coq.Classes.SetoidClass.
 
-(** 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.
 
 Class DecidableSetoid `(S : Setoid 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 `(S : Setoid A) :=
   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).
 
@@ -72,7 +75,8 @@ Infix "<>b" := nequiv_decb (no associativity, at level 70).
 
 Require Import Coq.Arith.Arith.
 
-(** 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 eq_setoid A : Setoid A | 10 :=
   { equiv := eq ; setoid_equiv := eq_equivalence }.
@@ -105,7 +109,8 @@ Program Instance prod_eqdec `(! EqDec (eq_setoid A), ! EqDec (eq_setoid B)) : Eq
 
   Solve Obligations using unfold complement ; program_simpl.
 
-(** Objects of function spaces with countable domains like bool have decidable equality. *)
+(** Objects of function spaces with countable domains like bool
+  have decidable equality. *)
 
 Program Instance bool_function_eqdec `(! EqDec (eq_setoid A)) : EqDec (eq_setoid (bool -> A)) :=
   λ f g,
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index 12356385c..c40e37e24 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -6,11 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* Tactics for typeclass-based setoids.
- *
- * Author: Matthieu Sozeau
- * Institution: LRI, CNRS UMR 8623 - Universit�copyright Paris Sud
- *              91405 Orsay, France *)
+(** * Tactics for typeclass-based setoids.
+
+   Author: Matthieu Sozeau
+   Institution: LRI, CNRS UMR 8623 - University Paris Sud
+*)
 
 (* $Id$ *)
 
@@ -34,12 +34,13 @@ Class DefaultRelation A (R : relation A).
 
 Definition default_relation `{DefaultRelation A R} := R.
 
-(** Every [Equivalence] gives a default relation, if no other is given (lowest priority). *)
+(** Every [Equivalence] gives a default relation, if no other is given
+  (lowest priority). *)
 
 Instance equivalence_default `(Equivalence A R) : DefaultRelation R | 4.
 
-(** The setoid_replace tactics in Ltac, defined in terms of default relations and
-   the setoid_rewrite tactic. *)
+(** The setoid_replace tactics in Ltac, defined in terms of default relations
+  and the setoid_rewrite tactic. *)
 
 Ltac setoidreplace H t :=
   let Heq := fresh "Heq" in
@@ -137,9 +138,11 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "by" tactic3(t) :=
   setoidreplaceinat (rel x y) id ltac:t o.
 
-(** The [add_morphism_tactic] tactic is run at each [Add Morphism] command before giving the hand back
-   to the user to discharge the proof. It essentially amounts to unfold the right amount of [respectful] calls
-   and substitute leibniz equalities. One can redefine it using [Ltac add_morphism_tactic ::= t]. *)
+(** The [add_morphism_tactic] tactic is run at each [Add Morphism]
+   command before giving the hand back to the user to discharge the
+   proof. It essentially amounts to unfold the right amount of
+   [respectful] calls and substitute leibniz equalities. One can
+   redefine it using [Ltac add_morphism_tactic ::= t]. *)
 
 Require Import Coq.Program.Tactics.