From b272730e00933e1542ee7209597ea1d35a001033 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sun, 29 Jul 2012 05:14:50 +0000
Subject: 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).
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15659 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/bigint.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'lib')

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
 
-- 
cgit v1.2.3