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

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.