aboutsummaryrefslogtreecommitdiff
path: root/kernel/retroknowledge.mli
diff options
context:
space:
mode:
authorVincent Laporte2018-09-07 12:22:17 +0200
committerVincent Laporte2018-09-14 07:51:17 +0000
commit42bed627c4a1c5a1ecf59d4865fc872b5eee7290 (patch)
treee70eab9f85e1f0c7d3818ac4d7c4712ffcc85483 /kernel/retroknowledge.mli
parentab2560233f2e6fc8c26853af6991533d8d335e16 (diff)
Retroknowledge: simpler parsing rules
Diffstat (limited to 'kernel/retroknowledge.mli')
-rw-r--r--kernel/retroknowledge.mli2
1 files changed, 2 insertions, 0 deletions
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli
index 6b2c74e9df..1436f23739 100644
--- a/kernel/retroknowledge.mli
+++ b/kernel/retroknowledge.mli
@@ -48,6 +48,8 @@ type int31_field =
type field =
| KInt31 of int31_field
+val int31_field_of_string : string -> int31_field
+
(** This type represent an atomic action of the retroknowledge. It
is stored in the compiled libraries
As per now, there is only the possibility of registering things