diff options
Diffstat (limited to 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 1b4d932b59..fe028c073f 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -126,3 +126,12 @@ val safe_infer : safe_environment -> constr -> judgment * Univ.constraints val typing : safe_environment -> constr -> judgment + +(*spiwack: safe retroknowledge functionalities *) + +open Retroknowledge + +val retroknowledge : (retroknowledge-> 'a) -> safe_environment -> 'a + +val register : safe_environment -> field -> Retroknowledge.entry -> constr + -> safe_environment |