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

diff --git a/theories/Wellfounded/Union.v b/theories/Wellfounded/Union.v
index ebf4ba98e..fbb3d9e3c 100644
--- a/theories/Wellfounded/Union.v
+++ b/theories/Wellfounded/Union.v
@@ -17,9 +17,9 @@ Require Import Transitive_Closure.
 Section WfUnion.
   Variable A : Type.
   Variables R1 R2 : relation A.
-  
+
   Notation Union := (union A R1 R2).
-  
+
   Remark strip_commut :
     commut A R1 R2 ->
     forall x y:A,
@@ -29,7 +29,7 @@ Section WfUnion.
     induction 2 as [x y| x y z H0 IH1 H1 IH2]; intros.
     elim H with y x z; auto with sets; intros x0 H2 H3.
     exists x0; auto with sets.
-    
+
     elim IH1 with z0; auto with sets; intros.
     elim IH2 with x0; auto with sets; intros.
     exists x1; auto with sets.
@@ -50,7 +50,7 @@ Section WfUnion.
     elim H8; intros.
     apply H6; auto with sets.
     apply t_trans with x0; auto with sets.
-    
+
     elim strip_commut with x x0 y0; auto with sets; intros.
     apply Acc_inv_trans with x1; auto with sets.
     unfold union in |- *.
@@ -63,7 +63,7 @@ Section WfUnion.
     apply Acc_intro; auto with sets.
   Qed.
 
-  
+
   Theorem wf_union :
     commut A R1 R2 -> well_founded R1 -> well_founded R2 -> well_founded Union.
   Proof.