diff options
Diffstat (limited to 'checker/safe_typing.mli')
| -rw-r--r-- | checker/safe_typing.mli | 10 |
1 files changed, 3 insertions, 7 deletions
diff --git a/checker/safe_typing.mli b/checker/safe_typing.mli index 986393b29..cd2c06d20 100644 --- a/checker/safe_typing.mli +++ b/checker/safe_typing.mli @@ -33,12 +33,8 @@ sig type table type lightened_compiled_library - (** [load lpf get_table lcl] builds a compiled library from a + (** [load table lcl] builds a compiled library from a lightened library [lcl] by remplacing every index by its related - opaque terms inside the table obtained by [get_table ()]. - If [lpf] is unset then the table is considered empty, which - implies that [get_table] is not evaluated and every index - is replaced by [None] inside the compiled library. *) - val load : load_proof:bool -> (unit -> table) - -> lightened_compiled_library -> compiled_library + opaque terms inside [table]. *) + val load : table -> lightened_compiled_library -> compiled_library end |