diff options
Diffstat (limited to 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 31bb8143e..7ca033383 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -136,3 +136,5 @@ val retroknowledge : (retroknowledge-> 'a) -> safe_environment -> 'a val register : safe_environment -> field -> Retroknowledge.entry -> constr -> safe_environment + +val register_inline : constant -> safe_environment -> safe_environment |