diff options
| author | thery | 2007-05-30 08:41:06 +0000 |
|---|---|---|
| committer | thery | 2007-05-30 08:41:06 +0000 |
| commit | bc96f88c74b487a73bc3312074d114bff63692f4 (patch) | |
| tree | 49fe5e6b3296455758ca06be19c3c2aadeafee76 /theories/Ints | |
| parent | d5914ef6cb90e494471e1e21e1b7ba1b2c842db0 (diff) | |
mul_norm for Q fixed
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9871 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Ints')
| -rw-r--r-- | theories/Ints/num/QMake.v | 8 |
1 files changed, 3 insertions, 5 deletions
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. |