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

diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index 16733c3b8..dff556b98 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -120,12 +120,12 @@ Defined.
 Definition Qeq_bool x y :=
   (Zeq_bool (Qnum x * QDen y) (Qnum y * QDen x))%Z.
 
-Definition Qle_bool x y := 
+Definition Qle_bool x y :=
   (Zle_bool (Qnum x * QDen y) (Qnum y * QDen x))%Z.
 
 Lemma Qeq_bool_iff : forall x y, Qeq_bool x y = true <-> x == y.
 Proof.
-  unfold Qeq_bool, Qeq; intros. 
+  unfold Qeq_bool, Qeq; intros.
   symmetry; apply Zeq_is_eq_bool.
 Qed.
 
diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v
index c34423b4d..266d81e01 100644
--- a/theories/QArith/Qcanon.v
+++ b/theories/QArith/Qcanon.v
@@ -13,7 +13,7 @@ Require Import QArith.
 Require Import Znumtheory.
 Require Import Eqdep_dec.
 
-(** [Qc] : A canonical representation of rational numbers. 
+(** [Qc] : A canonical representation of rational numbers.
    based on the setoid representation [Q]. *)
 
 Record Qc : Set := Qcmake { this :> Q ; canon : Qred this = this }.
@@ -23,7 +23,7 @@ Bind Scope Qc_scope with Qc.
 Arguments Scope Qcmake [Q_scope].
 Open Scope Qc_scope.
 
-Lemma Qred_identity : 
+Lemma Qred_identity :
   forall q:Q, Zgcd (Qnum q) (QDen q) = 1%Z -> Qred q = q.
 Proof.
   unfold Qred; intros (a,b); simpl.
@@ -36,7 +36,7 @@ Proof.
   subst; simpl; auto.
 Qed.
 
-Lemma Qred_identity2 : 
+Lemma Qred_identity2 :
   forall q:Q, Qred q = q -> Zgcd (Qnum q) (QDen q) = 1%Z.
 Proof.
   unfold Qred; intros (a,b); simpl.
@@ -50,7 +50,7 @@ Proof.
   destruct g as [|g|g]; destruct bb as [|bb|bb]; simpl in *; try discriminate.
   f_equal.
   apply Pmult_reg_r with bb.
-  injection H2; intros. 
+  injection H2; intros.
   rewrite <- H0.
   rewrite H; simpl; auto.
   elim H1; auto.
@@ -70,7 +70,7 @@ Proof.
   apply Qred_correct.
 Qed.
 
-Definition Q2Qc (q:Q) : Qc := Qcmake (Qred q) (Qred_involutive q). 
+Definition Q2Qc (q:Q) : Qc := Qcmake (Qred q) (Qred_involutive q).
 Arguments Scope Q2Qc [Q_scope].
 Notation " !! " := Q2Qc : Qc_scope.
 
@@ -82,7 +82,7 @@ Proof.
   assert (H0:=Qred_complete _ _ H).
   assert (q = q') by congruence.
   subst q'.
-  assert (proof_q = proof_q'). 
+  assert (proof_q = proof_q').
   apply eq_proofs_unicity; auto; intros.
   repeat decide equality.
   congruence.
@@ -98,8 +98,8 @@ Notation Qcgt := (fun x y : Qc => Qlt y x).
 Notation Qcge := (fun x y : Qc => Qle y x).
 Infix "<" := Qclt : Qc_scope.
 Infix "<=" := Qcle : Qc_scope.
-Infix ">" := Qcgt : Qc_scope. 
-Infix ">=" := Qcge : Qc_scope. 
+Infix ">" := Qcgt : Qc_scope.
+Infix ">=" := Qcge : Qc_scope.
 Notation "x <= y <= z" := (x<=y/\y<=z) : Qc_scope.
 Notation "x < y < z" := (x<y/\y<z) : Qc_scope.
 
@@ -141,9 +141,9 @@ Proof.
   intros.
   destruct (Qeq_dec x y) as [H|H]; auto.
   right; contradict H; subst; auto with qarith.
-Defined. 
+Defined.
 
-(** The addition, multiplication and opposite are defined 
+(** The addition, multiplication and opposite are defined
    in the straightforward way: *)
 
 Definition Qcplus (x y : Qc) := !!(x+y).
@@ -155,9 +155,9 @@ Notation "- x" := (Qcopp x) : Qc_scope.
 Definition Qcminus (x y : Qc) := x+-y.
 Infix "-" := Qcminus : Qc_scope.
 Definition Qcinv (x : Qc) := !!(/x).
-Notation "/ x" := (Qcinv x) : Qc_scope. 
+Notation "/ x" := (Qcinv x) : Qc_scope.
 Definition Qcdiv (x y : Qc) := x*/y.
-Infix "/" := Qcdiv : Qc_scope. 
+Infix "/" := Qcdiv : Qc_scope.
 
 (** [0] and [1] are apart *)
 
@@ -167,8 +167,8 @@ Proof.
   intros H; discriminate H.
 Qed.
 
-Ltac qc := match goal with 
- | q:Qc |- _ => destruct q; qc 
+Ltac qc := match goal with
+ | q:Qc |- _ => destruct q; qc
  | _ => apply Qc_is_canon; simpl; repeat rewrite Qred_correct
 end.
 
@@ -191,7 +191,7 @@ Qed.
 Lemma Qcplus_0_r : forall x, x+0 = x.
 Proof.
   intros; qc; apply Qplus_0_r.
-Qed. 
+Qed.
 
 (** Commutativity of addition: *)
 
@@ -265,13 +265,13 @@ Qed.
 Theorem Qcmult_integral_l : forall x y, ~ x = 0 -> x*y = 0 -> y = 0.
 Proof.
   intros; destruct (Qcmult_integral _ _ H0); tauto.
-Qed. 
+Qed.
 
-(** Inverse and division. *) 
+(** Inverse and division. *)
 
 Theorem Qcmult_inv_r : forall x, x<>0 -> x*(/x) = 1.
 Proof.
-  intros; qc; apply Qmult_inv_r; auto. 
+  intros; qc; apply Qmult_inv_r; auto.
 Qed.
 
 Theorem Qcmult_inv_l : forall x, x<>0 -> (/x)*x = 1.
@@ -436,24 +436,24 @@ Qed.
 Lemma Qcmult_lt_0_le_reg_r : forall x y z, 0 <  z  -> x*z <= y*z -> x <= y.
 Proof.
   unfold Qcmult, Qcle, Qclt; intros; simpl in *.
-  repeat progress rewrite Qred_correct in * |-. 
+  repeat progress rewrite Qred_correct in * |-.
   eapply Qmult_lt_0_le_reg_r; eauto.
 Qed.
 
 Lemma Qcmult_lt_compat_r : forall x y z, 0 < z  -> x < y -> x*z < y*z.
 Proof.
   unfold Qcmult, Qclt; intros; simpl in *.
-  repeat progress rewrite Qred_correct in *. 
+  repeat progress rewrite Qred_correct in *.
   eapply Qmult_lt_compat_r; eauto.
 Qed.
 
 (** Rational to the n-th power *)
 
-Fixpoint Qcpower (q:Qc)(n:nat) { struct n } : Qc := 
-  match n with 
+Fixpoint Qcpower (q:Qc)(n:nat) { struct n } : Qc :=
+  match n with
     | O => 1
     | S n => q * (Qcpower q n)
-  end. 
+  end.
 
 Notation " q ^ n " := (Qcpower q n) : Qc_scope.
 
@@ -467,7 +467,7 @@ Lemma Qcpower_0 : forall n, n<>O -> 0^n = 0.
 Proof.
   destruct n; simpl.
   destruct 1; auto.
-  intros. 
+  intros.
   apply Qc_is_canon.
   simpl.
   compute; auto.
@@ -537,7 +537,7 @@ Proof.
   intros (q, Hq) (q', Hq'); simpl; intros H.
   assert (H1 := H Hq Hq').
   subst q'.
-  assert (Hq = Hq'). 
+  assert (Hq = Hq').
   apply Eqdep_dec.eq_proofs_unicity; auto; intros.
   repeat decide equality.
   congruence.
diff --git a/theories/QArith/Qfield.v b/theories/QArith/Qfield.v
index 5373c1db3..fbfae55c3 100644
--- a/theories/QArith/Qfield.v
+++ b/theories/QArith/Qfield.v
@@ -73,15 +73,15 @@ Ltac Qpow_tac t :=
   | _ => NotConstant
   end.
 
-Add Field Qfield : Qsft 
- (decidable Qeq_bool_eq, 
+Add Field Qfield : Qsft
+ (decidable Qeq_bool_eq,
   completeness Qeq_eq_bool,
-  constants [Qcst], 
+  constants [Qcst],
   power_tac Qpower_theory [Qpow_tac]).
 
 (** Exemple of use: *)
 
-Section Examples. 
+Section Examples.
 
 Let ex1 : forall x y z : Q, (x+y)*z ==  (x*z)+(y*z).
   intros.
@@ -89,7 +89,7 @@ Let ex1 : forall x y z : Q, (x+y)*z ==  (x*z)+(y*z).
 Qed.
 
 Let ex2 : forall x y : Q, x+y == y+x.
-  intros. 
+  intros.
   ring.
 Qed.
 
diff --git a/theories/QArith/Qpower.v b/theories/QArith/Qpower.v
index efaefbb7c..fa341dd9c 100644
--- a/theories/QArith/Qpower.v
+++ b/theories/QArith/Qpower.v
@@ -59,7 +59,7 @@ Qed.
 
 Lemma Qmult_power : forall a b n, (a*b)^n == a^n*b^n.
 Proof.
-  intros a b [|n|n]; simpl; 
+  intros a b [|n|n]; simpl;
   try rewrite Qmult_power_positive;
   try rewrite Qinv_mult_distr;
   reflexivity.
@@ -73,7 +73,7 @@ Qed.
 
 Lemma Qinv_power : forall a n, (/a)^n == /a^n.
 Proof.
-  intros a [|n|n]; simpl; 
+  intros a [|n|n]; simpl;
   try rewrite Qinv_power_positive;
   reflexivity.
 Qed.
@@ -173,8 +173,8 @@ Qed.
 
 Lemma Qpower_mult : forall a n m, a^(n*m) ==  (a^n)^m.
 Proof.
-intros a [|n|n] [|m|m]; simpl; 
- try rewrite Qpower_positive_1; 
+intros a [|n|n] [|m|m]; simpl;
+ try rewrite Qpower_positive_1;
  try rewrite Qpower_mult_positive;
  try rewrite Qinv_power_positive;
  try rewrite Qinv_involutive;
diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v
index d57a8c824..12e371ee9 100644
--- a/theories/QArith/Qreals.v
+++ b/theories/QArith/Qreals.v
@@ -173,7 +173,7 @@ unfold Qinv, Q2R, Qeq in |- *; intros (x1, x2); unfold Qden, Qnum in |- *.
 case x1.
 simpl in |- *; intros; elim H; trivial.
 intros; field; auto.
-intros; 
+intros;
   change (IZR (Zneg x2)) with (- IZR (' x2))%R in |- *;
   change (IZR (Zneg p)) with (- IZR (' p))%R in |- *;
   field; (*auto 8 with real.*)
@@ -193,8 +193,8 @@ Hint Rewrite Q2R_plus Q2R_mult Q2R_opp Q2R_minus Q2R_inv Q2R_div : q2r_simpl.
 Section LegacyQField.
 
 (** In the past, the field tactic was not able to deal with setoid datatypes,
-    so translating from Q to R and applying field on reals was a workaround. 
-    See now Qfield for a direct field tactic on Q. *) 
+    so translating from Q to R and applying field on reals was a workaround.
+    See now Qfield for a direct field tactic on Q. *)
 
 Ltac QField := apply eqR_Qeq; autorewrite with q2r_simpl; try field; auto.
 
diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v
index 6b16cfff4..27e3c4e02 100644
--- a/theories/QArith/Qreduction.v
+++ b/theories/QArith/Qreduction.v
@@ -35,15 +35,15 @@ Qed.
 (** Simplification of fractions using [Zgcd].
   This version can compute within Coq. *)
 
-Definition Qred (q:Q) := 
-  let (q1,q2) := q in 
-  let (r1,r2) := snd (Zggcd q1 ('q2)) 
+Definition Qred (q:Q) :=
+  let (q1,q2) := q in
+  let (r1,r2) := snd (Zggcd q1 ('q2))
   in r1#(Z2P r2).
 
 Lemma Qred_correct : forall q, (Qred q) == q.
 Proof.
   unfold Qred, Qeq; intros (n,d); simpl.
-  generalize (Zggcd_gcd n ('d)) (Zgcd_is_pos n ('d)) 
+  generalize (Zggcd_gcd n ('d)) (Zgcd_is_pos n ('d))
     (Zgcd_is_gcd n ('d)) (Zggcd_correct_divisors n ('d)).
   destruct (Zggcd n (Zpos d)) as (g,(nn,dd)); simpl.
   Open Scope Z_scope.
@@ -52,7 +52,7 @@ Proof.
   rewrite H3; rewrite H4.
   assert (0 <> g).
   intro; subst g; discriminate.
-  
+
   assert (0 < dd).
   apply Zmult_gt_0_lt_0_reg_r with g.
   omega.
@@ -68,10 +68,10 @@ Proof.
   intros (a,b) (c,d).
   unfold Qred, Qeq in *; simpl in *.
   Open Scope Z_scope.
-  generalize (Zggcd_gcd a ('b)) (Zgcd_is_gcd a ('b)) 
+  generalize (Zggcd_gcd a ('b)) (Zgcd_is_gcd a ('b))
     (Zgcd_is_pos a ('b)) (Zggcd_correct_divisors a ('b)).
   destruct (Zggcd a (Zpos b)) as (g,(aa,bb)).
-  generalize (Zggcd_gcd c ('d)) (Zgcd_is_gcd c ('d)) 
+  generalize (Zggcd_gcd c ('d)) (Zgcd_is_gcd c ('d))
     (Zgcd_is_pos c ('d)) (Zggcd_correct_divisors c ('d)).
   destruct (Zggcd c (Zpos d)) as (g',(cc,dd)).
   simpl.
@@ -136,7 +136,7 @@ Proof.
   Close Scope Z_scope.
 Qed.
 
-Add Morphism Qred : Qred_comp. 
+Add Morphism Qred : Qred_comp.
 Proof.
   intros q q' H.
   rewrite (Qred_correct q); auto.
@@ -144,7 +144,7 @@ Proof.
 Qed.
 
 Definition Qplus' (p q : Q) := Qred (Qplus p q).
-Definition Qmult' (p q : Q) := Qred (Qmult p q). 
+Definition Qmult' (p q : Q) := Qred (Qmult p q).
 Definition Qminus' x y := Qred (Qminus x y).
 
 Lemma Qplus'_correct : forall p q : Q, (Qplus' p q)==(Qplus p q).