From d8e57d251feab8729f9282610854e1eaac4c92e4 Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 3 Aug 2012 09:26:34 +0000 Subject: [PATCH] Bigint: adds a missing -1 in hugo's last commit 15659 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.2@15670 85f007b7-540e-0410-9357-904b9bb8a0f7 --- lib/bigint.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/lib/bigint.ml b/lib/bigint.ml index bc98c9f28573..e96c66dc04b9 100644 --- a/lib/bigint.ml +++ b/lib/bigint.ml @@ -179,7 +179,10 @@ let rec can_divide k m d i = (m.(k+i) > d.(i)) or (m.(k+i) = d.(i) && can_divide k m d (i+1)) -(* computes m - d * q * base^(|m|-|d|-k) in-place on positive numbers *) +(* For two big nums m and d and a small number q, + computes m - d * q * base^(|m|-|d|-k) in-place (in m). + Both m d and q are positive. *) + let sub_mult m d q k = if q <> 0 then for i = Array.length d - 1 downto 0 do @@ -190,7 +193,7 @@ let sub_mult m d q k = m.(k+i-1) <- m.(k+i-1) - v / base; let j = ref (i-1) in while m.(k + !j) < 0 do (* result is positive, hence !j remains >= 0 *) - m.(k + !j) <- m.(k + !j) + base; decr j; m.(k + !j) <- m.(k + !j) + m.(k + !j) <- m.(k + !j) + base; decr j; m.(k + !j) <- m.(k + !j) -1 done end done