From bc96f88c74b487a73bc3312074d114bff63692f4 Mon Sep 17 00:00:00 2001
From: thery
Date: Wed, 30 May 2007 08:41:06 +0000
Subject: mul_norm for Q fixed

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9871 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Ints/num/QMake.v | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

(limited to 'theories')

diff --git a/theories/Ints/num/QMake.v b/theories/Ints/num/QMake.v
index 0fd20a1eb1..51451e82db 100644
--- a/theories/Ints/num/QMake.v
+++ b/theories/Ints/num/QMake.v
@@ -436,7 +436,7 @@ Definition mul_norm x y :=
        let zx := BigZ.div zx (BigZ.Pos gcd) in
        let d := BigN.div d gcd in
        if BigN.eq_bool d BigN.one then Qz (BigZ.mul zx ny)
-       else Qq (BigZ.mul zx ny) (BigN.pred d)
+       else Qq (BigZ.mul zx ny) d
  | Qq nx dx, Qz zy =>   
    if BigZ.eq_bool zy BigZ.zero then zero
    else	
@@ -447,10 +447,8 @@ Definition mul_norm x y :=
        let zy := BigZ.div zy (BigZ.Pos gcd) in
        let d := BigN.div d gcd in
        if BigN.eq_bool d BigN.one then Qz (BigZ.mul zy nx)
-       else Qq (BigZ.mul zy nx) (BigN.pred d)
+       else Qq (BigZ.mul zy nx) d
  | Qq nx dx, Qq ny dy => 
-     let dx := BigN.succ dx in
-     let dy := BigN.succ dy in
      let (nx, dy) := 
        let gcd := BigN.gcd (BigZ.to_N nx) dy in
        if BigN.eq_bool gcd BigN.one then (nx, dy)
@@ -461,7 +459,7 @@ Definition mul_norm x y :=
        else (BigZ.div ny (BigZ.Pos gcd), BigN.div dx gcd) in
      let d := (BigN.mul dx dy) in
      if BigN.eq_bool d BigN.one then Qz (BigZ.mul ny nx) 
-     else Qq (BigZ.mul ny nx) (BigN.pred d)
+     else Qq (BigZ.mul ny nx) d
  end.
 
 
-- 
cgit v1.2.3