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, 9 insertions, 9 deletions

diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v
index 9eef2bc1d..c5530e7ca 100644
--- a/theories/Setoids/Setoid.v
+++ b/theories/Setoids/Setoid.v
@@ -29,35 +29,35 @@ Definition Seq_trans A Aeq (s : Setoid_Theory A Aeq) : forall x y z:A, Aeq x y -
   unfold Setoid_Theory. intros ; transitivity y ; assumption.
 Defined.
 
-(** Some tactics for manipulating Setoid Theory not officially 
+(** Some tactics for manipulating Setoid Theory not officially
     declared as Setoid. *)
 
 Ltac trans_st x :=
   idtac "trans_st on Setoid_Theory is OBSOLETE";
   idtac "use transitivity on Equivalence instead";
   match goal with
-    | H : Setoid_Theory _ ?eqA |- ?eqA _ _ => 
+    | H : Setoid_Theory _ ?eqA |- ?eqA _ _ =>
       apply (Seq_trans _ _ H) with x; auto
   end.
 
 Ltac sym_st :=
   idtac "sym_st on Setoid_Theory is OBSOLETE";
   idtac "use symmetry on Equivalence instead";
-  match goal with 
-    | H : Setoid_Theory _ ?eqA |- ?eqA _ _ => 
+  match goal with
+    | H : Setoid_Theory _ ?eqA |- ?eqA _ _ =>
       apply (Seq_sym _ _ H); auto
   end.
 
 Ltac refl_st :=
   idtac "refl_st on Setoid_Theory is OBSOLETE";
   idtac "use reflexivity on Equivalence instead";
-  match goal with 
-    | H : Setoid_Theory _ ?eqA |- ?eqA _ _ => 
+  match goal with
+    | H : Setoid_Theory _ ?eqA |- ?eqA _ _ =>
       apply (Seq_refl _ _ H); auto
   end.
 
 Definition gen_st : forall A : Set, Setoid_Theory _ (@eq A).
-Proof. 
-  constructor; congruence. 
+Proof.
+  constructor; congruence.
 Qed.
-  
+