aboutsummaryrefslogtreecommitdiff
path: root/kernel/uint63_31.ml
diff options
context:
space:
mode:
authorGuillaume Melquiond2020-12-27 10:42:33 +0100
committerGuillaume Melquiond2021-01-10 10:24:10 +0100
commit944757e10651fda0d63d9291a6bcb1b6fdbaa256 (patch)
tree676b61021885d93290e74a1c9954e0dd80a3d9c2 /kernel/uint63_31.ml
parentd009572893913b889320f2fa3435543ee4c63f82 (diff)
Remove LSLINT63CONST1 and LSRINT63CONST1 as they are unused.
Diffstat (limited to 'kernel/uint63_31.ml')
-rw-r--r--kernel/uint63_31.ml2
1 files changed, 0 insertions, 2 deletions
diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml
index 988611df3e..4f2cbc4262 100644
--- a/kernel/uint63_31.ml
+++ b/kernel/uint63_31.ml
@@ -206,9 +206,7 @@ let () =
Callback.register "uint63 leq" le;
Callback.register "uint63 lor" l_or;
Callback.register "uint63 lsl" l_sl;
- Callback.register "uint63 lsl1" (fun x -> l_sl x Int64.one);
Callback.register "uint63 lsr" l_sr;
- Callback.register "uint63 lsr1" (fun x -> l_sr x Int64.one);
Callback.register "uint63 lt" lt;
Callback.register "uint63 lxor" l_xor;
Callback.register "uint63 mod" rem;