Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 10 insertions, 10 deletions

diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v
index 9c522f09..27e3c4e0 100644
--- a/theories/QArith/Qreduction.v
+++ b/theories/QArith/Qreduction.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Qreduction.v 10739 2008-04-01 14:45:20Z herbelin $ i*)
+(*i $Id$ i*)
 
 (** Normalisation functions for rational numbers. *)
 
@@ -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).