From 46ccc81a1de4ea3334e7b28b9e02cb5eaa5a7bf2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Tue, 23 Jul 2019 16:58:12 +0200
Subject: [PATCH] [WP] Fix typing errors during export with driver which use
builtins
---
src/kernel_internals/typing/logic_builtin.ml | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/src/kernel_internals/typing/logic_builtin.ml b/src/kernel_internals/typing/logic_builtin.ml
index ae1a73a9713..355bb752958 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
--
GitLab