diff options
| author | Vincent Laporte | 2018-09-10 13:20:39 +0200 |
|---|---|---|
| committer | Vincent Laporte | 2018-09-14 07:51:17 +0000 |
| commit | 736842d4cde09c667837dee8a633ff98ecf6a820 (patch) | |
| tree | f1004d1f56eca42109bba0a0680527c217e15264 /kernel | |
| parent | 2ec78477c720ba3a5343b49f25cfa9c1639adbba (diff) | |
Register: simpler syntax
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/retroknowledge.ml | 2 | ||||
| -rw-r--r-- | kernel/retroknowledge.mli | 2 |
2 files changed, 4 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} diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index 1fc3cfb817..0a2ef5300e 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -47,6 +47,8 @@ type field = val int31_field_of_string : string -> int31_field +val int31_path : DirPath.t + (** 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 |