Delete trailing whitespaces in all *.{v,ml*} files

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

1 files changed, 11 insertions, 11 deletions

diff --git a/test-suite/ideal-features/implicit_binders.v b/test-suite/ideal-features/implicit_binders.v
index 5b66944b5..2ec727808 100644
--- a/test-suite/ideal-features/implicit_binders.v
+++ b/test-suite/ideal-features/implicit_binders.v
@@ -1,8 +1,8 @@
 (** * Questions de syntaxe autour de la généralisation implicite
 
    ** Lieurs de classes
-   Aujourd'hui, les lieurs de classe [ ] et les 
-   lieurs {{ }} sont équivalents et on a toutes les combinaisons de { et ( pour 
+   Aujourd'hui, les lieurs de classe [ ] et les
+   lieurs {{ }} sont équivalents et on a toutes les combinaisons de { et ( pour
    les lieurs de classes (où la variable liée peut être anonyme):
    *)
 
@@ -22,7 +22,7 @@ Definition bar₄ {( F : Foo A )} (x y : A) := foo x + foo y.
 
 (** Les lieurs sont généralisés à tous les termes, pas seulement aux classes: *)
 
-Definition relation A := A -> A -> Prop. 
+Definition relation A := A -> A -> Prop.
 
 Definition inverse {( R : relation A )} := fun x y => R y x.
 
@@ -43,7 +43,7 @@ Definition inverse {( R : relation A )} := fun x y => R y x.
    [Definition inverse _{R : relation A} := fun x y => R y x]
 
    [Definition inverse `(R : relation A) := fun x y => R y x] et
-   
+
    [Definition inverse `[R : relation A] := fun x y => R y x] ou
    [Definition inverse `{R : relation A} := fun x y => R y x]
 
@@ -53,7 +53,7 @@ Definition inverse {( R : relation A )} := fun x y => R y x.
 
 Definition div (x : nat) ({ y <> 0 }) := 0.
 
-(** Un choix à faire pour les inductifs: accepter ou non de ne pas donner de nom à 
+(** Un choix à faire pour les inductifs: accepter ou non de ne pas donner de nom à
    l'argument. Manque de variables anonymes pour l'utilisateur mais pas pour le système... *)
 
 Inductive bla [ Foo A ] : Type :=.
@@ -73,10 +73,10 @@ Definition instimpl ({ SomeStruct a }) : nat := a + a.
 
 (** Donne l'instance explicitement (façon foncteur). *)
 
-Definition foo_prod {( Foo A, Foo B )} : Foo (A * B) := 
+Definition foo_prod {( Foo A, Foo B )} : Foo (A * B) :=
   fun x => let (l, r) := x in foo l + foo r.
 
-(** *** Questions: 
+(** *** Questions:
    - Gardez les crochets [ ] pour {{ }} ?
    - Quelle syntaxe pour la généralisation ?
    - Veut-on toutes les combinaisons de statut pour les variables généralisées et la variable liée ?
@@ -98,12 +98,12 @@ Definition baz := `{x + y + z = x + (y + z)}.
 Print baz.
 
 (** Proposition d'Arthur C.: déclarer les noms de variables généralisables à la [Implicit Types]
-   pour plus de robustesse (cela vaudrait aussi pour les lieurs). Les typos du genre de l'exemple suivant 
+   pour plus de robustesse (cela vaudrait aussi pour les lieurs). Les typos du genre de l'exemple suivant
    ne sont plus silencieuses: *)
 
 Check `(foob 0 + x).
 
-(** Utilisé pour généraliser l'implémentation de la généralisation implicite dans 
+(** Utilisé pour généraliser l'implémentation de la généralisation implicite dans
    les déclarations d'instances (i.e. les deux defs suivantes sont équivalentes). *)
 
 Instance fooa : Foo A.
@@ -111,8 +111,8 @@ Admitted.
 Definition fooa' : `(Foo A).
 Admitted.
 
-(** Un peu différent de la généralisation des lieurs qui "explosent" les variables 
-   libres en les liant au même niveau que l'objet. Dans la deuxième defs [a] n'est pas lié dans 
+(** Un peu différent de la généralisation des lieurs qui "explosent" les variables
+   libres en les liant au même niveau que l'objet. Dans la deuxième defs [a] n'est pas lié dans
    la définition mais [F : Π a, SomeStruct a]. *)
 
 Definition qux {( F : SomeStruct a )} : nat := a.