diff options
author | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-06-12 07:38:27 +0000 |
---|---|---|
committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-06-12 07:38:27 +0000 |
commit | d86f17ae08aaac00f81865d5b3f0e1e7c44119e1 (patch) | |
tree | 695de2b3f88bfc9911b77f56e91e16795776eea9 | |
parent | 3ef576e0c9a09384742cddb6f752d22784c267e3 (diff) |
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
-rw-r--r-- | plugins/setoid_ring/Ncring_polynom.v | 2 | ||||
-rw-r--r-- | test-suite/micromega/example.v | 4 | ||||
-rw-r--r-- | test-suite/success/Case11.v | 4 | ||||
-rw-r--r-- | test-suite/success/MatchFail.v | 2 | ||||
-rw-r--r-- | test-suite/success/TestRefine.v | 4 | ||||
-rw-r--r-- | test-suite/success/evars.v | 2 | ||||
-rw-r--r-- | test-suite/success/implicit.v | 2 | ||||
-rw-r--r-- | test-suite/success/instantiate.v | 2 | ||||
-rw-r--r-- | test-suite/success/ltac.v | 6 | ||||
-rw-r--r-- | test-suite/success/refine.v | 6 | ||||
-rw-r--r-- | test-suite/typeclasses/NewSetoid.v | 2 |
11 files changed, 18 insertions, 18 deletions
diff --git a/plugins/setoid_ring/Ncring_polynom.v b/plugins/setoid_ring/Ncring_polynom.v index c0d315871..17dd2daa3 100644 --- a/plugins/setoid_ring/Ncring_polynom.v +++ b/plugins/setoid_ring/Ncring_polynom.v @@ -103,7 +103,7 @@ Variable P:Pol. (* Xi^n * P + Q les variables de tete de Q ne sont pas forcement < i -mais Q est normalisé : variables de tete decroissantes *) +mais Q est normalisé : variables de tete decroissantes *) Fixpoint PaddX (i n:positive)(Q:Pol){struct Q}:= match Q with 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. |