diff options
Diffstat (limited to 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 8f86123c0..7cddde954 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -101,14 +101,16 @@ val delta_of_senv : safe_environment -> delta_resolver*delta_resolver (** exporting and importing modules *) type compiled_library +type native_library = Nativecode.global list + val start_library : Dir_path.t -> safe_environment -> module_path * safe_environment val export : safe_environment -> Dir_path.t - -> module_path * compiled_library + -> module_path * compiled_library * native_library val import : compiled_library -> Digest.t -> safe_environment - -> module_path * safe_environment + -> module_path * safe_environment * Nativecode.symbol array (** Remove the body of opaque constants *) |