diff options
Diffstat (limited to 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 1bb43a53e..cd24bd8d0 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -112,17 +112,6 @@ val export : safe_environment -> DirPath.t val import : compiled_library -> Digest.t -> safe_environment -> module_path * safe_environment * Nativecode.symbol array -(** Remove the body of opaque constants *) - -module LightenLibrary : -sig - type table - type lightened_compiled_library - val save : compiled_library -> lightened_compiled_library * table - val load : load_proof:Flags.load_proofs -> table Lazy.t -> - lightened_compiled_library -> compiled_library -end - (** {6 Typing judgments } *) type judgment |