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

2 files changed, 104 insertions, 104 deletions

diff --git a/theories/Numbers/Rational/BigQ/QMake.v b/theories/Numbers/Rational/BigQ/QMake.v
index 67411eac81..0973b7d8d9 100644
--- a/theories/Numbers/Rational/BigQ/QMake.v
+++ b/theories/Numbers/Rational/BigQ/QMake.v
@@ -28,27 +28,27 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
      number y interpreted as x/y. The pairs (x,0) and (0,y) are all
      interpreted as 0. *)
 
- Inductive t_ := 
+ Inductive t_ :=
   | Qz : Z.t -> t_
   | Qq : Z.t -> N.t -> t_.
 
  Definition t := t_.
 
- (** Specification with respect to [QArith] *) 
+ (** Specification with respect to [QArith] *)
 
  Open Local Scope Q_scope.
 
  Definition of_Z x: t := Qz (Z.of_Z x).
 
- Definition of_Q (q:Q) : t := 
-  let (x,y) := q in 
-  match y with 
+ Definition of_Q (q:Q) : t :=
+  let (x,y) := q in
+  match y with
     | 1%positive => Qz (Z.of_Z x)
     | _ => Qq (Z.of_Z x) (N.of_N (Npos y))
   end.
 
- Definition to_Q (q: t) := 
- match q with 
+ Definition to_Q (q: t) :=
+ match q with
    | Qz x => Z.to_Z x # 1
    | Qq x y => if N.eq_bool y N.zero then 0
                else Z.to_Z x # Z2P (N.to_Z y)
@@ -59,11 +59,11 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Theorem strong_spec_of_Q: forall q: Q, [of_Q q] = q.
  Proof.
  intros(x,y); destruct y; simpl; rewrite Z.spec_of_Z; auto.
- generalize (N.spec_eq_bool (N.of_N (Npos y~1)) N.zero); 
+ generalize (N.spec_eq_bool (N.of_N (Npos y~1)) N.zero);
   case N.eq_bool; auto; rewrite N.spec_0.
  rewrite N.spec_of_N; discriminate.
  rewrite N.spec_of_N; auto.
- generalize (N.spec_eq_bool (N.of_N (Npos y~0)) N.zero); 
+ generalize (N.spec_eq_bool (N.of_N (Npos y~0)) N.zero);
   case N.eq_bool; auto; rewrite N.spec_0.
  rewrite N.spec_of_N; discriminate.
  rewrite N.spec_of_N; auto.
@@ -98,77 +98,77 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Definition compare (x y: t) :=
   match x, y with
   | Qz zx, Qz zy => Z.compare zx zy
-  | Qz zx, Qq ny dy => 
+  | Qz zx, Qq ny dy =>
     if N.eq_bool dy N.zero then Z.compare zx Z.zero
     else Z.compare (Z.mul zx (Z_of_N dy)) ny
-  | Qq nx dx, Qz zy => 
-    if N.eq_bool dx N.zero then Z.compare Z.zero zy 
+  | Qq nx dx, Qz zy =>
+    if N.eq_bool dx N.zero then Z.compare Z.zero zy
     else Z.compare nx (Z.mul zy (Z_of_N dx))
   | Qq nx dx, Qq ny dy =>
     match N.eq_bool dx N.zero, N.eq_bool dy N.zero with
     | true, true => Eq
     | true, false => Z.compare Z.zero ny
     | false, true => Z.compare nx Z.zero
-    | false, false => Z.compare (Z.mul nx (Z_of_N dy)) 
+    | false, false => Z.compare (Z.mul nx (Z_of_N dy))
                                 (Z.mul ny (Z_of_N dx))
     end
   end.
 
- Lemma Zcompare_spec_alt : 
+ Lemma Zcompare_spec_alt :
   forall z z', Z.compare z z' = (Z.to_Z z ?= Z.to_Z z')%Z.
  Proof.
  intros; generalize (Z.spec_compare z z'); destruct Z.compare; auto.
  intro H; rewrite H; symmetry; apply Zcompare_refl.
  Qed.
- 
- Lemma Ncompare_spec_alt : 
+
+ Lemma Ncompare_spec_alt :
   forall n n', N.compare n n' = (N.to_Z n ?= N.to_Z n')%Z.
  Proof.
  intros; generalize (N.spec_compare n n'); destruct N.compare; auto.
  intro H; rewrite H; symmetry; apply Zcompare_refl.
  Qed.
 
- Lemma N_to_Z2P : forall n, N.to_Z n <> 0%Z -> 
+ Lemma N_to_Z2P : forall n, N.to_Z n <> 0%Z ->
   Zpos (Z2P (N.to_Z n)) = N.to_Z n.
  Proof.
  intros; apply Z2P_correct.
  generalize (N.spec_pos n); romega.
  Qed.
 
- Hint Rewrite 
-  Zplus_0_r Zplus_0_l Zmult_0_r Zmult_0_l Zmult_1_r Zmult_1_l 
+ Hint Rewrite
+  Zplus_0_r Zplus_0_l Zmult_0_r Zmult_0_l Zmult_1_r Zmult_1_l
   Z.spec_0 N.spec_0 Z.spec_1 N.spec_1 Z.spec_m1 Z.spec_opp
   Zcompare_spec_alt Ncompare_spec_alt
-  Z.spec_add N.spec_add Z.spec_mul N.spec_mul 
+  Z.spec_add N.spec_add Z.spec_mul N.spec_mul
   Z.spec_gcd N.spec_gcd Zgcd_Zabs Zgcd_1
   spec_Z_of_N spec_Zabs_N
  : nz.
  Ltac nzsimpl := autorewrite with nz in *.
 
  Ltac destr_neq_bool := repeat
- (match goal with |- context [N.eq_bool ?x ?y] => 
+ (match goal with |- context [N.eq_bool ?x ?y] =>
    generalize (N.spec_eq_bool x y); case N.eq_bool
   end).
- 
+
  Ltac destr_zeq_bool := repeat
- (match goal with |- context [Z.eq_bool ?x ?y] => 
+ (match goal with |- context [Z.eq_bool ?x ?y] =>
    generalize (Z.spec_eq_bool x y); case Z.eq_bool
   end).
 
  Ltac simpl_ndiv := rewrite N.spec_div by (nzsimpl; romega).
- Tactic Notation "simpl_ndiv" "in" "*" := 
+ Tactic Notation "simpl_ndiv" "in" "*" :=
    rewrite N.spec_div in * by (nzsimpl; romega).
 
  Ltac simpl_zdiv := rewrite Z.spec_div by (nzsimpl; romega).
- Tactic Notation "simpl_zdiv" "in" "*" := 
+ Tactic Notation "simpl_zdiv" "in" "*" :=
    rewrite Z.spec_div in * by (nzsimpl; romega).
 
- Ltac qsimpl := try red; unfold to_Q; simpl; intros; 
+ Ltac qsimpl := try red; unfold to_Q; simpl; intros;
   destr_neq_bool; destr_zeq_bool; simpl; nzsimpl; auto; intros.
 
  Theorem spec_compare: forall q1 q2, (compare q1 q2) = ([q1] ?= [q2]).
  Proof.
- intros [z1 | x1 y1] [z2 | x2 y2]; 
+ intros [z1 | x1 y1] [z2 | x2 y2];
    unfold Qcompare, compare; qsimpl; rewrite ! N_to_Z2P; auto.
  Qed.
 
@@ -177,7 +177,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Definition min n m := match compare n m with Gt => m | _ => n end.
  Definition max n m := match compare n m with Lt => m | _ => n end.
 
- Definition eq_bool n m := 
+ Definition eq_bool n m :=
   match compare n m with Eq => true | _ => false end.
 
  Theorem spec_eq_bool: forall x y,
@@ -196,9 +196,9 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  (** Normalisation function *)
 
  Definition norm n d : t :=
-  let gcd := N.gcd (Zabs_N n) d in 
+  let gcd := N.gcd (Zabs_N n) d in
   match N.compare N.one gcd with
-  | Lt => 
+  | Lt =>
     let n := Z.div n (Z_of_N gcd) in
     let d := N.div d gcd in
     match N.compare d N.one with
@@ -249,7 +249,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Theorem strong_spec_norm : forall p q, [norm p q] = Qred [Qq p q].
  Proof.
  intros.
- replace (Qred [Qq p q]) with (Qred [norm p q]) by 
+ replace (Qred [Qq p q]) with (Qred [norm p q]) by
   (apply Qred_complete; apply spec_norm).
  symmetry; apply Qred_identity.
  unfold norm.
@@ -282,10 +282,10 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  simpl; auto with zarith.
  Qed.
 
- (** Reduction function : producing irreducible fractions *) 
+ (** Reduction function : producing irreducible fractions *)
 
- Definition red (x : t) : t := 
-  match x with 
+ Definition red (x : t) : t :=
+  match x with
    | Qz z => x
    | Qq n d => norm n d
   end.
@@ -307,18 +307,18 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  symmetry; apply Qred_identity; simpl; auto with zarith.
  unfold red; apply strong_spec_norm.
  Qed.
-   
+
  Definition add (x y: t): t :=
   match x with
   | Qz zx =>
     match y with
     | Qz zy => Qz (Z.add zx zy)
-    | Qq ny dy => 
-      if N.eq_bool dy N.zero then x 
+    | Qq ny dy =>
+      if N.eq_bool dy N.zero then x
       else Qq (Z.add (Z.mul zx (Z_of_N dy)) ny) dy
     end
   | Qq nx dx =>
-    if N.eq_bool dx N.zero then y 
+    if N.eq_bool dx N.zero then y
     else match y with
     | Qz zy => Qq (Z.add nx (Z.mul zy (Z_of_N dx))) dx
     | Qq ny dy =>
@@ -352,12 +352,12 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
   | Qz zx =>
     match y with
     | Qz zy => Qz (Z.add zx zy)
-    | Qq ny dy =>  
-      if N.eq_bool dy N.zero then x 
+    | Qq ny dy =>
+      if N.eq_bool dy N.zero then x
       else norm (Z.add (Z.mul zx (Z_of_N dy)) ny) dy
     end
   | Qq nx dx =>
-    if N.eq_bool dx N.zero then y 
+    if N.eq_bool dx N.zero then y
     else match y with
     | Qz zy => norm (Z.add nx (Z.mul zy (Z_of_N dx))) dx
     | Qq ny dy =>
@@ -372,16 +372,16 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Theorem spec_add_norm : forall x y, [add_norm x y] == [x] + [y].
  Proof.
  intros x y; rewrite <- spec_add.
- destruct x; destruct y; unfold add_norm, add; 
+ destruct x; destruct y; unfold add_norm, add;
  destr_neq_bool; auto using Qeq_refl, spec_norm.
  Qed.
 
- Theorem strong_spec_add_norm : forall x y : t, 
+ Theorem strong_spec_add_norm : forall x y : t,
    Reduced x -> Reduced y -> Reduced (add_norm x y).
  Proof.
  unfold Reduced; intros.
  rewrite strong_spec_red.
- rewrite <- (Qred_complete [add x y]); 
+ rewrite <- (Qred_complete [add x y]);
   [ | rewrite spec_add, spec_add_norm; apply Qeq_refl ].
  rewrite <- strong_spec_red.
  destruct x as [zx|nx dx]; destruct y as [zy|ny dy].
@@ -404,7 +404,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Proof.
  intros [z | x y]; simpl.
  rewrite Z.spec_opp; auto.
- match goal with  |- context[N.eq_bool ?X ?Y] => 
+ match goal with  |- context[N.eq_bool ?X ?Y] =>
   generalize (N.spec_eq_bool X Y); case N.eq_bool
  end; auto; rewrite N.spec_0.
  rewrite Z.spec_opp; auto.
@@ -438,7 +438,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  rewrite spec_opp; ring.
  Qed.
 
- Theorem strong_spec_sub_norm : forall x y, 
+ Theorem strong_spec_sub_norm : forall x y,
   Reduced x -> Reduced y -> Reduced (sub_norm x y).
  Proof.
  intros.
@@ -470,7 +470,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
   generalize (N.spec_pos dy); omega.
  Qed.
 
- Lemma norm_denum : forall n d, 
+ Lemma norm_denum : forall n d,
   [if N.eq_bool d N.one then Qz n else Qq n d] == [Qq n d].
  Proof.
  intros; simpl; qsimpl.
@@ -478,15 +478,15 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  rewrite N_to_Z2P, H0; auto with zarith.
  Qed.
 
- Definition irred n d :=        
+ Definition irred n d :=
    let gcd := N.gcd (Zabs_N n) d in
-   match N.compare gcd N.one with 
+   match N.compare gcd N.one with
      | Gt => (Z.div n (Z_of_N gcd), N.div d gcd)
      | _ => (n, d)
    end.
 
- Lemma spec_irred : forall n d, exists g, 
-  let (n',d') := irred n d in 
+ Lemma spec_irred : forall n d, exists g,
+  let (n',d') := irred n d in
   (Z.to_Z n' * g = Z.to_Z n)%Z /\ (N.to_Z d' * g = N.to_Z d)%Z.
  Proof.
  intros.
@@ -511,7 +511,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  rewrite Zmult_comm; symmetry; apply Zdivide_Zdiv_eq; auto with zarith.
  Qed.
 
- Lemma spec_irred_zero : forall n d, 
+ Lemma spec_irred_zero : forall n d,
    (N.to_Z d = 0)%Z <-> (N.to_Z (snd (irred n d)) = 0)%Z.
  Proof.
  intros.
@@ -535,8 +535,8 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  compute in H1; elim H1; auto.
  Qed.
 
- Lemma strong_spec_irred : forall n d, 
-  (N.to_Z d <> 0%Z) -> 
+ Lemma strong_spec_irred : forall n d,
+  (N.to_Z d <> 0%Z) ->
   let (n',d') := irred n d in Zgcd (Z.to_Z n') (N.to_Z d') = 1%Z.
  Proof.
  unfold irred; intros.
@@ -554,31 +554,31 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  apply Zgcd_is_gcd; auto.
  Qed.
 
- Definition mul_norm_Qz_Qq z n d := 
-   if Z.eq_bool z Z.zero then zero 
+ Definition mul_norm_Qz_Qq z n d :=
+   if Z.eq_bool z Z.zero then zero
    else
     let gcd := N.gcd (Zabs_N z) d in
     match N.compare gcd N.one with
-      | Gt => 
+      | Gt =>
         let z := Z.div z (Z_of_N gcd) in
         let d := N.div d gcd in
         if N.eq_bool d N.one then Qz (Z.mul z n) else Qq (Z.mul z n) d
       | _  => Qq (Z.mul z n) d
     end.
 
- Definition mul_norm (x y: t): t := 
+ Definition mul_norm (x y: t): t :=
  match x, y with
  | Qz zx, Qz zy => Qz (Z.mul zx zy)
  | Qz zx, Qq ny dy => mul_norm_Qz_Qq zx ny dy
  | Qq nx dx, Qz zy => mul_norm_Qz_Qq zy nx dx
- | Qq nx dx, Qq ny dy => 
-    let (nx, dy) := irred nx dy in 
-    let (ny, dx) := irred ny dx in 
+ | Qq nx dx, Qq ny dy =>
+    let (nx, dy) := irred nx dy in
+    let (ny, dx) := irred ny dx in
     let d := N.mul dx dy in
     if N.eq_bool d N.one then Qz (Z.mul ny nx) else Qq (Z.mul ny nx) d
  end.
 
- Lemma spec_mul_norm_Qz_Qq : forall z n d, 
+ Lemma spec_mul_norm_Qz_Qq : forall z n d,
    [mul_norm_Qz_Qq z n d] == [Qq (Z.mul z n) d].
  Proof.
  intros z n d; unfold mul_norm_Qz_Qq; nzsimpl; rewrite Zcompare_gt.
@@ -599,14 +599,14 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  rewrite <- Zgcd_div_swap0; auto with zarith; ring.
  Qed.
 
- Lemma strong_spec_mul_norm_Qz_Qq : forall z n d, 
+ Lemma strong_spec_mul_norm_Qz_Qq : forall z n d,
    Reduced (Qq n d) -> Reduced (mul_norm_Qz_Qq z n d).
  Proof.
  unfold Reduced; intros z n d.
  rewrite 2 strong_spec_red, 2 Qred_iff.
  simpl; nzsimpl.
  destr_neq_bool; intros Hd H; simpl in *; nzsimpl.
- 
+
  unfold mul_norm_Qz_Qq; nzsimpl; rewrite Zcompare_gt.
  destr_zeq_bool; intros Hz; simpl; nzsimpl; simpl; auto.
  destruct Z_le_gt_dec.
@@ -670,7 +670,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  destruct (spec_irred ny dx) as (g' & Hg').
  assert (Hz := spec_irred_zero nx dy).
  assert (Hz':= spec_irred_zero ny dx).
- destruct irred as (n1,d1); destruct irred as (n2,d2). 
+ destruct irred as (n1,d1); destruct irred as (n2,d2).
  simpl snd in *; destruct Hg as [Hg1 Hg2]; destruct Hg' as [Hg1' Hg2'].
  rewrite norm_denum.
  qsimpl.
@@ -686,10 +686,10 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  rewrite 2 Z2P_correct.
  rewrite <- Hg1, <- Hg2, <- Hg1', <- Hg2'; ring.
 
- assert (0 <= N.to_Z d2 * N.to_Z d1)%Z 
+ assert (0 <= N.to_Z d2 * N.to_Z d1)%Z
   by (apply Zmult_le_0_compat; apply N.spec_pos).
  romega.
- assert (0 <= N.to_Z dx * N.to_Z dy)%Z 
+ assert (0 <= N.to_Z dx * N.to_Z dy)%Z
   by (apply Zmult_le_0_compat; apply N.spec_pos).
  romega.
  Qed.
@@ -712,7 +712,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  assert (Hz':= spec_irred_zero ny dx).
  assert (Hgc := strong_spec_irred nx dy).
  assert (Hgc' := strong_spec_irred ny dx).
- destruct irred as (n1,d1); destruct irred as (n2,d2). 
+ destruct irred as (n1,d1); destruct irred as (n2,d2).
  simpl snd in *; destruct Hg as [Hg1 Hg2]; destruct Hg' as [Hg1' Hg2'].
  destr_neq_bool; simpl; nzsimpl; intros; auto.
  destr_neq_bool; simpl; nzsimpl; intros; auto.
@@ -729,7 +729,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
 
  apply Zgcd_mult_rel_prime; rewrite Zgcd_comm;
   apply Zgcd_mult_rel_prime; rewrite Zgcd_comm; auto.
- 
+
  rewrite Zgcd_1_rel_prime in *.
  apply bezout_rel_prime.
  destruct (rel_prime_bezout _ _ H4) as [u v Huv].
@@ -747,15 +747,15 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  romega.
  Qed.
 
- Definition inv (x: t): t := 
+ Definition inv (x: t): t :=
  match x with
- | Qz z => 
-   match Z.compare Z.zero z with 
+ | Qz z =>
+   match Z.compare Z.zero z with
      | Eq => zero
      | Lt => Qq Z.one (Zabs_N z)
      | Gt => Qq Z.minus_one (Zabs_N z)
    end
- | Qq n d => 
+ | Qq n d =>
    match Z.compare Z.zero n with
      | Eq => zero
      | Lt => Qq (Z_of_N d) (Zabs_N n)
@@ -827,25 +827,25 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  rewrite T, Zpos_mult_morphism, N_to_Z2P; auto; ring.
  Qed.
 
- Definition inv_norm (x: t): t := 
+ Definition inv_norm (x: t): t :=
    match x with
-     | Qz z => 
-       match Z.compare Z.zero z with 
+     | Qz z =>
+       match Z.compare Z.zero z with
          | Eq => zero
          | Lt => Qq Z.one (Zabs_N z)
          | Gt => Qq Z.minus_one (Zabs_N z)
        end
-     | Qq n d => 
-       if N.eq_bool d N.zero then zero else 
-       match Z.compare Z.zero n with 
+     | Qq n d =>
+       if N.eq_bool d N.zero then zero else
+       match Z.compare Z.zero n with
          | Eq => zero
-         | Lt => 
-           match Z.compare n Z.one with 
+         | Lt =>
+           match Z.compare n Z.one with
              | Gt => Qq (Z_of_N d) (Zabs_N n)
              | _ => Qz (Z_of_N d)
            end
-         | Gt => 
-           match Z.compare n Z.minus_one with 
+         | Gt =>
+           match Z.compare n Z.minus_one with
              | Lt => Qq (Z.opp (Z_of_N d)) (Zabs_N n)
              | _ => Qz (Z.opp (Z_of_N d))
            end
@@ -882,7 +882,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
 
  Theorem strong_spec_inv_norm : forall x, Reduced x -> Reduced (inv_norm x).
  Proof.
- unfold Reduced. 
+ unfold Reduced.
  intros.
  destruct x as [ z | n d ].
  (* Qz *)
@@ -952,8 +952,8 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  apply Qeq_refl.
  apply spec_inv_norm; auto.
  Qed.
- 
- Theorem strong_spec_div_norm : forall x y, 
+
+ Theorem strong_spec_div_norm : forall x y,
    Reduced x -> Reduced y -> Reduced (div_norm x y).
  Proof.
  intros; unfold div_norm.
@@ -980,7 +980,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  rewrite H in H0; simpl in H0; elim H0; auto.
  assert (0 < N.to_Z d)%Z by (generalize (N.spec_pos d); romega).
  clear H H0.
- rewrite Z.spec_square, N.spec_square.  
+ rewrite Z.spec_square, N.spec_square.
  red; simpl.
  rewrite Zpos_mult_morphism; rewrite !Z2P_correct; auto.
  apply Zmult_lt_0_compat; auto.
@@ -991,7 +991,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
   | Qz zx => Qz (Z.power_pos zx p)
   | Qq nx dx => Qq (Z.power_pos nx p) (N.power_pos dx p)
   end.
- 
+
  Theorem spec_power_pos : forall x p, [power_pos x p] == [x] ^ Zpos p.
  Proof.
  intros [ z | n d ] p; unfold power_pos.
@@ -1019,7 +1019,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  rewrite N.spec_power_pos. auto.
  Qed.
 
- Theorem strong_spec_power_pos : forall x p, 
+ Theorem strong_spec_power_pos : forall x p,
   Reduced x -> Reduced (power_pos x p).
  Proof.
  destruct x as [z | n d]; simpl; intros.
@@ -1040,8 +1040,8 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  apply rel_prime_Zpower; auto with zarith.
  Qed.
 
- Definition power (x : t) (z : Z) : t := 
-   match z with 
+ Definition power (x : t) (z : Z) : t :=
+   match z with
      | Z0 => one
      | Zpos p => power_pos x p
      | Zneg p => inv (power_pos x p)
@@ -1056,8 +1056,8 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  rewrite spec_inv, spec_power_pos; apply Qeq_refl.
  Qed.
 
- Definition power_norm (x : t) (z : Z) : t := 
-   match z with 
+ Definition power_norm (x : t) (z : Z) : t :=
+   match z with
      | Z0 => one
      | Zpos p => power_pos x p
      | Zneg p => inv_norm (power_pos x p)
@@ -1072,7 +1072,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  rewrite spec_inv_norm, spec_power_pos; apply Qeq_refl.
  Qed.
 
- Theorem strong_spec_power_norm : forall x z, 
+ Theorem strong_spec_power_norm : forall x z,
    Reduced x -> Reduced (power_norm x z).
  Proof.
  destruct z; simpl.
@@ -1085,7 +1085,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
 
 
  (** Interaction with [Qcanon.Qc] *)
- 
+
  Open Scope Qc_scope.
 
  Definition of_Qc q := of_Q (this q).
@@ -1166,7 +1166,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  apply Qplus_comp; apply Qeq_sym; apply Qred_correct.
  Qed.
 
- Theorem spec_add_normc_bis : forall x y : Qc, 
+ Theorem spec_add_normc_bis : forall x y : Qc,
    [add_norm (of_Qc x) (of_Qc y)] = x+y.
  Proof.
  intros.
@@ -1189,7 +1189,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  rewrite spec_oppc; ring.
  Qed.
 
- Theorem spec_sub_normc_bis : forall x y : Qc, 
+ Theorem spec_sub_normc_bis : forall x y : Qc,
    [sub_norm (of_Qc x) (of_Qc y)] = x-y.
  Proof.
  intros.
@@ -1228,7 +1228,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  apply Qmult_comp; apply Qeq_sym; apply Qred_correct.
  Qed.
 
- Theorem spec_mul_normc_bis : forall x y : Qc, 
+ Theorem spec_mul_normc_bis : forall x y : Qc,
    [mul_norm (of_Qc x) (of_Qc y)] = x*y.
  Proof.
  intros.
@@ -1266,7 +1266,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  apply Qinv_comp; apply Qeq_sym; apply Qred_correct.
  Qed.
 
- Theorem spec_inv_normc_bis : forall x : Qc, 
+ Theorem spec_inv_normc_bis : forall x : Qc,
    [inv_norm (of_Qc x)] = /x.
  Proof.
  intros.
@@ -1280,7 +1280,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Proof.
  intros x y; unfold div; rewrite spec_mulc; auto.
  unfold Qcdiv; apply f_equal2 with (f := Qcmult); auto.
- apply spec_invc; auto. 
+ apply spec_invc; auto.
  Qed.
 
  Theorem spec_div_normc x y: [[div_norm x y]] = [[x]] / [[y]].
@@ -1290,7 +1290,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  apply spec_inv_normc; auto.
  Qed.
 
- Theorem spec_div_normc_bis : forall x y : Qc, 
+ Theorem spec_div_normc_bis : forall x y : Qc,
    [div_norm (of_Qc x) (of_Qc y)] = x/y.
  Proof.
  intros.
diff --git a/theories/Numbers/Rational/SpecViaQ/QSig.v b/theories/Numbers/Rational/SpecViaQ/QSig.v
index 7c88d25aae..8be66493e5 100644
--- a/theories/Numbers/Rational/SpecViaQ/QSig.v
+++ b/theories/Numbers/Rational/SpecViaQ/QSig.v
@@ -48,12 +48,12 @@ Module Type QType.
  Definition max n m := match compare n m with Lt => m | _ => n end.
 
  Parameter eq_bool : t -> t -> bool.
- 
- Parameter spec_eq_bool : forall x y, 
+
+ Parameter spec_eq_bool : forall x y,
   if eq_bool x y then [x]==[y] else ~([x]==[y]).
 
  Parameter red : t -> t.
- 
+
  Parameter spec_red : forall x, [red x] == [x].
  Parameter strong_spec_red : forall x, [red x] = Qred [x].