diff --git a/src/kernel_internals/typing/logic_builtin.ml b/src/kernel_internals/typing/logic_builtin.ml index ae1a73a97132d659383b01a7ec8643a7f72c002d..355bb752958e52dbc0ab03853b166d9e6683e30a 100644 --- a/src/kernel_internals/typing/logic_builtin.ml +++ b/src/kernel_internals/typing/logic_builtin.ml @@ -161,7 +161,8 @@ let init = "\\pointer_comparable", [], [], [("p1", fun_ptr); ("p2", object_ptr)]; "\\pointer_comparable", [], [], [("p1", object_ptr); - ("p2", fun_ptr)]; + ("p2", fun_ptr)]; + "\\bit_test", [], [], ["x", Linteger; "pos", Linteger] ; ]; (* functions *) List.iter