aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGuillaume Melquiond2020-12-01 18:28:43 +0100
committerGuillaume Melquiond2020-12-01 18:28:43 +0100
commit9ca7e769b62173a79a1c7d12a363205dd608b519 (patch)
tree5b4d3fa900f4d4d49db7732101b735ff0aef4acc
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.
-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)