diff options
Diffstat (limited to 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 0ab70b69e..3a7954874 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -114,10 +114,11 @@ val import : compiled_library -> Digest.t -> safe_environment module LightenLibrary : sig - type table - type lightened_compiled_library + type table + type lightened_compiled_library val save : compiled_library -> lightened_compiled_library * table - val load : load_proof:bool -> (unit -> table) -> lightened_compiled_library -> compiled_library + val load : load_proof:Flags.load_proofs -> table Lazy.t -> + lightened_compiled_library -> compiled_library end (** {6 Typing judgments } *) @@ -135,8 +136,6 @@ val safe_infer : safe_environment -> constr -> judgment * Univ.constraints val typing : safe_environment -> constr -> judgment - - (*spiwack: safe retroknowledge functionalities *) open Retroknowledge |