Changed encoding from ISO-8859-1 to UTF-8 for some remaining gallina files.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15431 85f007b7-540e-0410-9357-904b9bb8a0f7

10 files changed, 17 insertions, 17 deletions

diff --git a/test-suite/micromega/example.v b/test-suite/micromega/example.v
index f424f0fcc..f5a953566 100644
--- a/test-suite/micromega/example.v
+++ b/test-suite/micromega/example.v
@@ -2,7 +2,7 @@
 (*                                                                      *)
 (* Micromega: A reflexive tactic using the Positivstellensatz           *)
 (*                                                                      *)
-(*  Frédéric Besson (Irisa/Inria) 2006-2008                             *)
+(*  Frédéric Besson (Irisa/Inria) 2006-2008                             *)
 (*                                                                      *)
 (************************************************************************)
 
@@ -23,7 +23,7 @@ Proof.
 Qed.
 
 
-(* From Laurent Théry *)
+(* From Laurent Théry *)
 
 Lemma some_pol : forall x, 4 * x ^ 2 + 3 * x + 2 >= 0.
 Proof.
diff --git a/test-suite/success/Case11.v b/test-suite/success/Case11.v
index fd5d139c6..c8f772687 100644
--- a/test-suite/success/Case11.v
+++ b/test-suite/success/Case11.v
@@ -1,5 +1,5 @@
-(* L'algo d'inférence du prédicat doit gérer le K-rédex dans le type de b *)
-(* Problème rapporté par Solange Coupet *)
+(* L'algo d'inférence du prédicat doit gérer le K-rédex dans le type de b *)
+(* Problème rapporté par Solange Coupet *)
 
 Section A.
 
diff --git a/test-suite/success/MatchFail.v b/test-suite/success/MatchFail.v
index 660ca3cb0..d43cd0e87 100644
--- a/test-suite/success/MatchFail.v
+++ b/test-suite/success/MatchFail.v
@@ -4,7 +4,7 @@ Require Export ZArithRing.
 (* Cette tactique a pour objectif de remplacer toute instance
    de (POS (xI e)) ou de (POS (xO e)) par
    2*(POS e)+1  ou 2*(POS e), pour rendre les expressions plus
-   à même d'être utilisées par Ring, lorsque ces expressions contiennent
+   à même d'être utilisées par Ring, lorsque ces expressions contiennent
    des variables de type positive. *)
 Ltac compute_POS :=
   match goal with
diff --git a/test-suite/success/TestRefine.v b/test-suite/success/TestRefine.v
index 705bdc45c..852f3da81 100644
--- a/test-suite/success/TestRefine.v
+++ b/test-suite/success/TestRefine.v
@@ -119,7 +119,7 @@ Lemma essai : {x : nat | x = 1}.
 Restart.
 
 (* mais si on contraint par le but alors ca marche : *)
-(* Remarque : on peut toujours faire ça *)
+(* Remarque : on peut toujours faire ça *)
  refine (exist _ 1 _:{x : nat | x = 1}).
 
 Restart.
@@ -184,7 +184,7 @@ Qed.
 
 
 
-(* Quelques essais de recurrence bien fondée *)
+(* Quelques essais de recurrence bien fondée *)
 
 Require Import Wf.
 Require Import Wf_nat.
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index e6088091b..ceb940a45 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -44,7 +44,7 @@ Fixpoint build (nl : list nat) :
 
 
 (* Checks that disjoint contexts are correctly set by restrict_hyp *)
-(* Bug de 1999 corrigé en déc 2004 *)
+(* Bug de 1999 corrigé en déc 2004 *)
 
 Check
   (let p :=
diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v
index e8019a908..a0981311b 100644
--- a/test-suite/success/implicit.v
+++ b/test-suite/success/implicit.v
@@ -61,7 +61,7 @@ Check (eq1 0 0).
 Check (eq2 0 0).
 Check (eq3 nat 0 0).
 
-(* Example submitted by Frédéric (interesting in v8 syntax) *)
+(* Example submitted by Frédéric (interesting in v8 syntax) *)
 
 Parameter f : nat -> nat * nat.
 Notation lhs := fst.
diff --git a/test-suite/success/instantiate.v b/test-suite/success/instantiate.v
index 4224405d9..6f1030a43 100644
--- a/test-suite/success/instantiate.v
+++ b/test-suite/success/instantiate.v
@@ -1,4 +1,4 @@
-(* Test régression bug #1041 *)
+(* Test régression bug #1041 *)
 
 Goal Prop.
 
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index 7387add6a..0c8a18167 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -1,6 +1,6 @@
 (* The tactic language *)
 
-(* Submitted by Pierre Crégut *)
+(* Submitted by Pierre Crégut *)
 (* Checks substitution of x *)
 Ltac f x := unfold x in |- *; idtac.
 
@@ -9,7 +9,7 @@ f plus.
 reflexivity.
 Qed.
 
-(* Submitted by Pierre Crégut *)
+(* Submitted by Pierre Crégut *)
 (* Check syntactic correctness *)
 Ltac F x := idtac; G x
  with G y := idtac; F y.
@@ -211,7 +211,7 @@ is.
 exact I.
 Abort.
 
-(* Interférence entre espaces des noms *)
+(* Interférence entre espaces des noms *)
 
 Ltac O := intro.
 Ltac Z1 t := set (x:=t).
diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v
index 4d743a6d7..8b4f41055 100644
--- a/test-suite/success/refine.v
+++ b/test-suite/success/refine.v
@@ -67,9 +67,9 @@ Abort.
 
 (* Submitted by Jacek Chrzaszcz (bug #1102) *)
 
-(* le problème a été résolu ici par normalisation des evars présentes
-   dans les types d'evars, mais le problème reste a priori ouvert dans
-   le cas plus général d'evars non instanciées dans les types d'autres
+(* le problème a été résolu ici par normalisation des evars présentes
+   dans les types d'evars, mais le problème reste a priori ouvert dans
+   le cas plus général d'evars non instanciées dans les types d'autres
    evars *)
 
 Goal exists n:nat, n=n.
diff --git a/test-suite/typeclasses/NewSetoid.v b/test-suite/typeclasses/NewSetoid.v
index 3fdcce6f7..22ac77a68 100644
--- a/test-suite/typeclasses/NewSetoid.v
+++ b/test-suite/typeclasses/NewSetoid.v
@@ -8,7 +8,7 @@
 
 (* Certified Haskell Prelude.
  * Author: Matthieu Sozeau
- * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
+ * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
  *              91405 Orsay, France *)
 
 Require Import Coq.Program.Program.