aboutsummaryrefslogtreecommitdiff
path: root/kernel/retroknowledge.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/retroknowledge.ml')
-rw-r--r--kernel/retroknowledge.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index c1a8820bf0..e51c25c06b 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -80,6 +80,8 @@ let int31_field_of_string =
| "lxor" -> Int31Lxor
| s -> CErrors.user_err Pp.(str "Registering unknown int31 operator " ++ str s)
+let int31_path = DirPath.make [ Id.of_string "int31" ]
+
(* record representing all the flags of the internal state of the kernel *)
type flags = {fastcomputation : bool}