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

diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v
index a52df1bfc..51c2a2905 100644
--- a/theories/ZArith/Zabs.v
+++ b/theories/ZArith/Zabs.v
@@ -77,9 +77,9 @@ Proof.
       (intros H2; rewrite H2); auto.
 Qed.
 
-Lemma Zabs_spec : forall x:Z, 
-  0 <= x /\ Zabs x = x \/ 
-  0 > x /\ Zabs x = -x. 
+Lemma Zabs_spec : forall x:Z,
+  0 <= x /\ Zabs x = x \/
+  0 > x /\ Zabs x = -x.
 Proof.
  intros; unfold Zabs, Zle, Zgt; destruct x; simpl; intuition discriminate.
 Qed.
@@ -142,7 +142,7 @@ Lemma Zabs_nat_mult: forall n m:Z, Zabs_nat (n*m) = (Zabs_nat n * Zabs_nat m)%na
 Proof.
   intros; apply inj_eq_rev.
   rewrite inj_mult; repeat rewrite inj_Zabs_nat; apply Zabs_Zmult.
-Qed. 
+Qed.
 
 Lemma Zabs_nat_Zsucc:
  forall p, 0 <= p ->  Zabs_nat (Zsucc p) = S (Zabs_nat p).
@@ -151,13 +151,13 @@ Proof.
   rewrite inj_S; repeat rewrite inj_Zabs_nat, Zabs_eq; auto with zarith.
 Qed.
 
-Lemma Zabs_nat_Zplus: 
+Lemma Zabs_nat_Zplus:
  forall x y, 0<=x -> 0<=y -> Zabs_nat (x+y) = (Zabs_nat x + Zabs_nat y)%nat.
 Proof.
   intros; apply inj_eq_rev.
   rewrite inj_plus; repeat rewrite inj_Zabs_nat, Zabs_eq; auto with zarith.
   apply Zplus_le_0_compat; auto.
-Qed.  
+Qed.
 
 Lemma Zabs_nat_Zminus:
  forall x y, 0 <= x <= y ->  Zabs_nat (y - x) = (Zabs_nat y - Zabs_nat x)%nat.
@@ -200,11 +200,11 @@ Qed.
 
 (** A characterization of the sign function: *)
 
-Lemma Zsgn_spec : forall x:Z, 
-  0 < x /\ Zsgn x = 1 \/ 
-  0 = x /\ Zsgn x = 0 \/ 
+Lemma Zsgn_spec : forall x:Z,
+  0 < x /\ Zsgn x = 1 \/
+  0 = x /\ Zsgn x = 0 \/
   0 > x /\ Zsgn x = -1.
-Proof. 
+Proof.
  intros; unfold Zsgn, Zle, Zgt; destruct x; compute; intuition.
 Qed.