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

@@ -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