From 736842d4cde09c667837dee8a633ff98ecf6a820 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Mon, 10 Sep 2018 13:20:39 +0200
Subject: Register: simpler syntax

---
 kernel/retroknowledge.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'kernel/retroknowledge.ml')

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}
 
-- 
cgit v1.2.3