diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/uint63_31.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml index ddb6ba656e..445166f6af 100644 --- a/kernel/uint63_31.ml +++ b/kernel/uint63_31.ml @@ -132,6 +132,7 @@ let mulc x y = (* add the outer products *) let lr = Int64.add (Int64.mul lx ly) lr in let hr = Int64.add (Int64.mul hx hy) hr in + (* hr fits on 64 bits, since the final result fits on 126 bits *) (* now x * y = hr * 2^62 + lr and lr < 2^63 *) let lr = Int64.add lr (Int64.shift_left (Int64.logand hr 1L) 62) in let hr = Int64.shift_right_logical hr 1 in |