aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorGuillaume Melquiond2020-12-01 18:28:43 +0100
committerGuillaume Melquiond2020-12-01 18:28:43 +0100
commit9ca7e769b62173a79a1c7d12a363205dd608b519 (patch)
tree5b4d3fa900f4d4d49db7732101b735ff0aef4acc /kernel
parent33c42201b9d44d8772e65f336feb72b38469c079 (diff)
Make the code clearer and faster by calling mask63 explicitly at the end.
Before this commit, function mask63 was called implicitly at each step.
Diffstat (limited to 'kernel')
-rw-r--r--kernel/uint63_31.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml
index 5b2d934b5d..696efacb32 100644
--- a/kernel/uint63_31.ml
+++ b/kernel/uint63_31.ml
@@ -72,12 +72,12 @@ let l_xor x y = Int64.logxor x y
(* addition of int63 *)
let add x y = mask63 (Int64.add x y)
-let addcarry x y = add (add x y) Int64.one
+let addcarry x y = mask63 Int64.(add (add x y) one)
(* subtraction *)
let sub x y = mask63 (Int64.sub x y)
-let subcarry x y = sub (sub x y) Int64.one
+let subcarry x y = mask63 Int64.(sub (sub x y) one)
(* multiplication *)
let mul x y = mask63 (Int64.mul x y)