3 files changed, 17 insertions, 16 deletions
diff --git a/kernel/byterun/coq_uint63_native.h b/kernel/byterun/coq_uint63_native.h
index ffa52dc63b..9fbd3f83d8 100644
--- a/kernel/byterun/coq_uint63_native.h
+++ b/kernel/byterun/coq_uint63_native.h
@@ -111,14 +111,12 @@ value uint63_mulc(value x, value y, value* h) {
 #define le128(xh,xl,yh,yl) (uint63_lt(xh,yh) || (uint63_eq(xh,yh) && uint63_leq(xl,yl)))
 
 #define maxuint63 ((uint64_t)0x7FFFFFFFFFFFFFFF)
-/* precondition: y <> 0 */
-/* outputs r and sets ql to q % 2^63 s.t. x = q * y + r, r < y */
+/* precondition: xh < y */
+/* outputs r and sets ql to q s.t. x = q * y + r, r < y */
 static value uint63_div21_aux(value xh, value xl, value y, value* ql) {
-  xh = uint63_of_value(xh);
-  xl = uint63_of_value(xl);
+  uint64_t nh = uint63_of_value(xh);
+  uint64_t nl = uint63_of_value(xl);
   y = uint63_of_value(y);
-  uint64_t nh = xh % y;
-  uint64_t nl = xl;
   uint64_t q = 0;
   for (int i = 0; i < 63; ++i) {
     // invariants: 0 <= nh < y, nl = (xl*2^i) % 2^64,
@@ -132,7 +130,7 @@ static value uint63_div21_aux(value xh, value xl, value y, value* ql) {
   return Val_int(nh);
 }
 value uint63_div21(value xh, value xl, value y, value* ql) {
-  if (uint63_of_value(y) == 0) {
+  if (uint63_leq(y, xh)) {
     *ql = Val_int(0);
     return Val_int(0);
   } else {
diff --git a/kernel/uint63_amd64_63.ml b/kernel/uint63_amd64_63.ml
index 1bb633d413..98560e8b95 100644
--- a/kernel/uint63_amd64_63.ml
+++ b/kernel/uint63_amd64_63.ml
@@ -95,13 +95,12 @@ let le (x : int) (y : int) =
 [@@ocaml.inline always]
 
     (* division of two numbers by one *)
-(* precondition: y <> 0 *)
-(* outputs: q % 2^63, r s.t. x = q * y + r, r < y *)
+(* precondition: xh < y *)
+(* outputs: q, r s.t. x = q * y + r, r < y *)
 let div21 xh xl y =
-  let y = to_uint64 y in
   (* nh might temporarily grow as large as 2*y - 1 in the loop body,
      so we store it as a 64-bit unsigned integer *)
-  let nh = ref (Int64.rem (to_uint64 xh) y) in
+  let nh = ref xh in
   let nl = ref xl in
   let q = ref 0 in
   for _i = 0 to 62 do
@@ -117,7 +116,10 @@ let div21 xh xl y =
   done;
   !q, Int64.to_int !nh
 
-let div21 xh xl y = if y = 0 then 0, 0 else div21 xh xl y
+let div21 xh xl y =
+  let xh = to_uint64 xh in
+  let y = to_uint64 y in
+  if Int64.compare y xh <= 0 then 0, 0 else div21 xh xl y
 
      (* exact multiplication *)
 (* TODO: check that none of these additions could be a logical or *)
diff --git a/kernel/uint63_i386_31.ml b/kernel/uint63_i386_31.ml
index 91a1e397a8..2306427b03 100644
--- a/kernel/uint63_i386_31.ml
+++ b/kernel/uint63_i386_31.ml
@@ -87,10 +87,10 @@ let addmuldiv p x y =
   l_or (l_sl x p) (l_sr y Int64.(sub (of_int uint_size) p))
 
     (* division of two numbers by one *)
-(* precondition: y <> 0 *)
-(* outputs: q % 2^63, r s.t. x = q * y + r, r < y *)
+(* precondition: xh < y *)
+(* outputs: q, r s.t. x = q * y + r, r < y *)
 let div21 xh xl y =
-  let nh = ref (Int64.rem xh y) in
+  let nh = ref xh in
   let nl = ref xl in
   let q = ref 0L in
   for _i = 0 to 62 do
@@ -106,7 +106,8 @@ let div21 xh xl y =
   done;
   !q, !nh
 
-let div21 xh xl y = if Int64.equal y zero then zero, zero else div21 xh xl y
+let div21 xh xl y =
+  if Int64.compare y xh <= 0 then zero, zero else div21 xh xl y
 
      (* exact multiplication *)
 let mulc x y =