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

6 files changed, 20 insertions, 20 deletions

diff --git a/test-suite/micromega/example.v b/test-suite/micromega/example.v
index 5cb103953..f424f0fcc 100644
--- a/test-suite/micromega/example.v
+++ b/test-suite/micromega/example.v
@@ -19,7 +19,7 @@ Lemma not_so_easy : forall x n : Z,
   2*x + 1 <= 2 *n -> x <= n-1.
 Proof.
   intros.
-  lia. 
+  lia.
 Qed.
 
 
@@ -27,19 +27,19 @@ Qed.
 
 Lemma some_pol : forall x, 4 * x ^ 2 + 3 * x + 2 >= 0.
 Proof.
-  intros. 
+  intros.
   psatz Z 2.
 Qed.
 
 
-Lemma Zdiscr: forall a b c x, 
+Lemma Zdiscr: forall a b c x,
   a * x ^ 2 + b * x + c = 0 -> b ^ 2 - 4 * a * c >= 0.
 Proof.
   intros ; psatz Z 4.
 Qed.
 
 
-Lemma plus_minus : forall x y, 
+Lemma plus_minus : forall x y,
   0 = x + y -> 0 =  x -y -> 0 = x /\ 0 = y.
 Proof.
   intros.
@@ -48,20 +48,20 @@ Qed.
 
 
 
-Lemma mplus_minus : forall x y, 
+Lemma mplus_minus : forall x y,
   x + y >= 0 -> x -y >= 0 -> x^2 - y^2 >= 0.
 Proof.
   intros; psatz Z 2.
 Qed.
 
-Lemma pol3: forall x y, 0 <= x + y ->  
+Lemma pol3: forall x y, 0 <= x + y ->
   x^3 + 3*x^2*y + 3*x* y^2 + y^3 >= 0.
 Proof.
   intros; psatz Z 4.
 Qed.
 
 
-(* Motivating example from: Expressiveness + Automation + Soundness: 
+(* Motivating example from: Expressiveness + Automation + Soundness:
    Towards COmbining SMT Solvers and Interactive Proof Assistants *)
 Parameter rho : Z.
 Parameter rho_ge : rho >= 0.
@@ -76,7 +76,7 @@ Definition rbound2 (C:Z -> Z -> Z) : Prop :=
 
 
 Lemma bounded_drift : forall s t p q C D, s <= t /\ correct p t  /\ correct q t /\
-  rbound1 C /\ rbound2 C /\ rbound1 D /\ rbound2 D  -> 
+  rbound1 C /\ rbound2 C /\ rbound1 D /\ rbound2 D  ->
   Zabs (C p t - D q t) <= Zabs (C p s - D q s) + 2 * rho * (t- s).
 Proof.
   intros.
@@ -194,8 +194,8 @@ Qed.
 (* from hol_light/Examples/sos.ml *)
 
 Lemma hol_light1 : forall a1 a2 b1 b2,
-  a1 >= 0 -> a2 >= 0 -> 
-   (a1 * a1 + a2 * a2 = b1 * b1 + b2 * b2 + 2) -> 
+  a1 >= 0 -> a2 >= 0 ->
+   (a1 * a1 + a2 * a2 = b1 * b1 + b2 * b2 + 2) ->
    (a1 * b1 + a2 * b2 = 0) -> a1 * a2 - b1 * b2 >= 0.
 Proof.
   intros ; psatz Z 4.
@@ -323,7 +323,7 @@ Proof.
 Qed.
 
 
-Lemma hol_light24 : forall x1 y1 x2 y2, x1 >= 0 -> x2 >= 0 -> y1 >= 0 -> y2 >= 0 -> 
+Lemma hol_light24 : forall x1 y1 x2 y2, x1 >= 0 -> x2 >= 0 -> y1 >= 0 -> y2 >= 0 ->
   ((x1 + y1) ^2 + x1 + 1 = (x2 + y2) ^ 2 + x2 + 1)
                 -> (x1 + y1 = x2 + y2).
 Proof.
diff --git a/test-suite/micromega/heap3_vcgen_25.v b/test-suite/micromega/heap3_vcgen_25.v
index 0298303f5..efb5c7fd5 100644
--- a/test-suite/micromega/heap3_vcgen_25.v
+++ b/test-suite/micromega/heap3_vcgen_25.v
@@ -11,7 +11,7 @@ Require Import Psatz.
 
 Open Scope Z_scope.
 
-Lemma vcgen_25 : forall   
+Lemma vcgen_25 : forall
   (n : Z)
   (m : Z)
   (jt : Z)
diff --git a/test-suite/micromega/qexample.v b/test-suite/micromega/qexample.v
index 1fa250e09..c9c779f90 100644
--- a/test-suite/micromega/qexample.v
+++ b/test-suite/micromega/qexample.v
@@ -10,7 +10,7 @@ Require Import Psatz.
 Require Import QArith.
 Require Import Ring_normalize.
 
-Lemma plus_minus : forall x y, 
+Lemma plus_minus : forall x y,
   0 == x + y -> 0 ==  x -y -> 0 == x /\ 0 == y.
 Proof.
   intros.
@@ -37,7 +37,7 @@ Qed.
 Open Scope Z_scope.
 Open Scope Q_scope.
 
-Lemma vcgen_25 : forall   
+Lemma vcgen_25 : forall
   (n : Q)
   (m : Q)
   (jt : Q)
diff --git a/test-suite/micromega/rexample.v b/test-suite/micromega/rexample.v
index d7386a4ec..c957add69 100644
--- a/test-suite/micromega/rexample.v
+++ b/test-suite/micromega/rexample.v
@@ -12,7 +12,7 @@ Require Import Ring_normalize.
 
 Open Scope R_scope.
 
-Lemma yplus_minus : forall x y, 
+Lemma yplus_minus : forall x y,
   0 = x + y -> 0 =  x -y -> 0 = x /\ 0 = y.
 Proof.
   intros.
@@ -34,7 +34,7 @@ Proof.
 Qed.
 
 
-Lemma vcgen_25 : forall   
+Lemma vcgen_25 : forall
   (n : R)
   (m : R)
   (jt : R)
diff --git a/test-suite/micromega/square.v b/test-suite/micromega/square.v
index b78bba25c..4c00ffe4a 100644
--- a/test-suite/micromega/square.v
+++ b/test-suite/micromega/square.v
@@ -20,7 +20,7 @@ Proof.
 intros [n [p [Heq Hnz]]]; pose (n' := Zabs n); pose (p':=Zabs p).
 assert (facts : 0 <= Zabs n /\ 0 <= Zabs p /\ Zabs n^2=n^2
          /\ Zabs p^2 = p^2) by auto.
-assert (H : (0 < n' /\ 0 <= p' /\ n' ^2 = 2* p' ^2)) by 
+assert (H : (0 < n' /\ 0 <= p' /\ n' ^2 = 2* p' ^2)) by
   (destruct facts as [Hf1 [Hf2 [Hf3 Hf4]]]; unfold n', p' ; psatz Z 2).
 generalize p' H; elim n' using (well_founded_ind (Zwf_well_founded 0)); clear.
 intros n IHn p [Hn [Hp Heq]].
@@ -55,7 +55,7 @@ Theorem sqrt2_not_rational : ~exists x:Q, x^2==2#1.
 Proof.
  unfold Qeq; intros [x]; simpl (Qden (2#1)); rewrite Zmult_1_r.
  intros HQeq.
- assert (Heq : (Qnum x ^ 2 = 2 * ' Qden x ^ 2%Q)%Z) by 
+ assert (Heq : (Qnum x ^ 2 = 2 * ' Qden x ^ 2%Q)%Z) by
    (rewrite QnumZpower in HQeq ; rewrite QdenZpower in HQeq ; auto).
  assert (Hnx : (Qnum x <> 0)%Z)
  by (intros Hx; simpl in HQeq; rewrite Hx in HQeq; discriminate HQeq).
diff --git a/test-suite/micromega/zomicron.v b/test-suite/micromega/zomicron.v
index 60c16a998..3b2460233 100644
--- a/test-suite/micromega/zomicron.v
+++ b/test-suite/micromega/zomicron.v
@@ -24,7 +24,7 @@ Lemma omega_nightmare : forall x y, 27 <= 11 * x + 13 * y <= 45 ->  -10 <= 7 * x
 Proof.
   intros ; intuition auto.
   lia.
-Qed.  
+Qed.
 
 Lemma compact_proof : forall z,
  (z < 0) ->
@@ -32,5 +32,5 @@ Lemma compact_proof : forall z,
   (0 >= z \/ 0 < z) -> False.
 Proof.
  intros.
- lia. 
+ lia.
 Qed.
\ No newline at end of file