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

diff --git a/theories/Sets/Constructive_sets.v b/theories/Sets/Constructive_sets.v
index 65ce03e28..0719365f1 100644
--- a/theories/Sets/Constructive_sets.v
+++ b/theories/Sets/Constructive_sets.v
@@ -30,7 +30,7 @@ Require Export Ensembles.
 
 Section Ensembles_facts.
   Variable U : Type.
-  
+
   Lemma Extension : forall B C:Ensemble U, B = C -> Same_set U B C.
   Proof.
     intros B C H'; rewrite H'; auto with sets.
@@ -52,7 +52,7 @@ Section Ensembles_facts.
   Proof.
     unfold Add at 1 in |- *; auto with sets.
   Qed.
-  
+
   Lemma Add_intro2 : forall (A:Ensemble U) (x:U), In U (Add U A x) x.
   Proof.
     unfold Add at 1 in |- *; auto with sets.
@@ -98,15 +98,15 @@ Section Ensembles_facts.
   Proof.
     intros B C x H'; elim H'; auto with sets.
   Qed.
-  
+
   Lemma Add_inv :
     forall (A:Ensemble U) (x y:U), In U (Add U A x) y -> In U A y \/ x = y.
   Proof.
-    intros A x y H'; induction H'. 
+    intros A x y H'; induction H'.
       left; assumption.
       right; apply Singleton_inv; assumption.
   Qed.
-  
+
   Lemma Intersection_inv :
     forall (B C:Ensemble U) (x:U),
       In U (Intersection U B C) x -> In U B x /\ In U C x.
@@ -125,7 +125,7 @@ Section Ensembles_facts.
   Proof.
     unfold Setminus at 1 in |- *; red in |- *; auto with sets.
   Qed.
- 
+
   Lemma Strict_Included_intro :
     forall X Y:Ensemble U, Included U X Y /\ X <> Y -> Strict_Included U X Y.
   Proof.