diff options
Diffstat (limited to 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 7ca033383..210d601fb 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -26,6 +26,15 @@ type safe_environment val env_of_safe_env : safe_environment -> Environ.env +val sideff_of_con : safe_environment -> constant -> side_effect + +val is_curmod_library : safe_environment -> bool + + +(* safe_environment has functional data affected by lazy computations, + * thus this function returns a new safe_environment *) +val join_safe_environment : safe_environment -> safe_environment + val empty_environment : safe_environment val is_empty : safe_environment -> bool @@ -109,6 +118,8 @@ val export : safe_environment -> DirPath.t val import : compiled_library -> Digest.t -> safe_environment -> module_path * safe_environment * Nativecode.symbol array +val join_compiled_library : compiled_library -> unit + (** {6 Typing judgments } *) type judgment |