Better fixing propagation of carry in sub_mult used for euclidian

division over unbounded integers (thanks again to L. Théry for
pointing out the remaining problem in r15637).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15659 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 4 insertions, 2 deletions

diff --git a/lib/bigint.ml b/lib/bigint.ml
index 050046ec7..7fce6b815 100644
--- a/lib/bigint.ml
+++ b/lib/bigint.ml
@@ -184,8 +184,10 @@ let sub_mult m d q k =
     if m.(k+i) < 0 then (m.(k+i) <- m.(k+i) + base; m.(k+i-1) <- m.(k+i-1) -1);
     if v >= base then begin
       m.(k+i-1) <- m.(k+i-1) - v / base;
-      if m.(k+i-1) < 0 then
-        (m.(k+i-1) <- m.(k+i-1) + base; m.(k+i-2) <- m.(k+i-2) -1)
+      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)
+      done
     end
   done