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

4 files changed, 12 insertions, 10 deletions

diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 93b723af30..0fe8bb1764 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.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/Reals/Ranalysis3.v b/theories/Reals/Ranalysis3.v
index 3de97ba903..3b685cd8a0 100644
--- a/theories/Reals/Ranalysis3.v
+++ b/theories/Reals/Ranalysis3.v
@@ -60,7 +60,7 @@ Proof.
   case (Req_dec (f1 x) 0); intro.
   case (Req_dec l1 0); intro.
 (***********************************)
-(*              Cas n° 1           *)
+(*              First case         *)
 (*           (f1 x)=0  l1 =0       *)
 (***********************************)
   cut (0 < Rmin eps_f2 (Rmin alp_f2 alp_f1d));
@@ -118,7 +118,7 @@ Proof.
   apply Rmin_2; assumption.
   right; symmetry  in |- *; apply quadruple_var.
 (***********************************)
-(*              Cas n° 2           *)
+(*           Second case           *)
 (*           (f1 x)=0  l1<>0       *)
 (***********************************)
   assert (H10 := derivable_continuous_pt _ _ X).
@@ -218,7 +218,7 @@ Proof.
   apply Rinv_neq_0_compat; repeat apply prod_neq_R0;
     [ discrR | discrR | discrR | assumption ].
 (***********************************)
-(*              Cas n° 3           *)
+(*        Third case               *)
 (*     (f1 x)<>0  l1=0  l2=0       *)
 (***********************************)
   case (Req_dec l1 0); intro.
@@ -291,7 +291,7 @@ Proof.
   apply (cond_pos alp_f1d).
   apply (cond_pos alp_f2d).
 (***********************************)
-(*              Cas n° 4           *)
+(*      Fourth case                *)
 (*    (f1 x)<>0  l1=0  l2<>0       *)
 (***********************************)
   elim (H0 (Rabs (Rsqr (f2 x) * eps / (8 * f1 x))));
@@ -421,7 +421,7 @@ Proof.
   apply Rinv_neq_0_compat; discrR.
   apply Rinv_neq_0_compat; assumption.
 (***********************************)
-(*              Cas n° 5           *)
+(*         Fifth case              *)
 (*    (f1 x)<>0  l1<>0  l2=0       *)
 (***********************************)
   case (Req_dec l2 0); intro.
@@ -538,7 +538,7 @@ Proof.
         (apply Rinv_neq_0_compat; discrR) ||
           (red in |- *; intro H12; rewrite H12 in H6; elim (Rlt_irrefl _ H6)).
 (***********************************)
-(*              Cas n° 6           *)
+(*       Sixth case                *)
 (*    (f1 x)<>0  l1<>0  l2<>0      *)
 (***********************************)
   elim (H0 (Rabs (Rsqr (f2 x) * eps / (8 * f1 x)))).
diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v
index 88cead7a5f..63684c1f34 100644
--- a/theories/Reals/RiemannInt.v
+++ b/theories/Reals/RiemannInt.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 *)
@@ -423,7 +424,7 @@ Proof.
 Qed.
 
 (***************************************)
-(** C°([a,b]) is included in L1([a,b]) *)
+(** C°([a,b]) is included in L1([a,b]) *)
 (***************************************)
 
 Lemma maxN :
diff --git a/theories/Reals/Rtopology.v b/theories/Reals/Rtopology.v
index c115969e33..5b55896b17 100644
--- a/theories/Reals/Rtopology.v
+++ b/theories/Reals/Rtopology.v
@@ -1598,17 +1598,17 @@ Theorem Heine :
     (forall x:R, X x -> continuity_pt f x) -> uniform_continuity f X.
 Proof.
   intros f0 X H0 H; elim (domain_P1 X); intro Hyp.
-(* X est vide *)
+(* X is empty *)
   unfold uniform_continuity in |- *; intros; exists (mkposreal _ Rlt_0_1);
     intros; elim Hyp; exists x; assumption.
   elim Hyp; clear Hyp; intro Hyp.
-(* X possède un seul élément *)
+(* X has only one element *)
   unfold uniform_continuity in |- *; intros; exists (mkposreal _ Rlt_0_1);
     intros; elim Hyp; clear Hyp; intros; elim H4; clear H4;
       intros; assert (H6 := H5 _ H1); assert (H7 := H5 _ H2);
         rewrite H6; rewrite H7; unfold Rminus in |- *; rewrite Rplus_opp_r;
           rewrite Rabs_R0; apply (cond_pos eps).
-(* X possède au moins deux éléments distincts *)
+(* X has at least two distinct elements *)
   assert
     (X_enc :
       exists m : R, (exists M : R, (forall x:R, X x -> m <= x <= M) /\ m < M)).