diff options
| author | Gaëtan Gilbert | 2019-06-11 11:22:24 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-06-11 11:22:24 +0200 |
| commit | 793a442d240c22f99591388ad31e33fbaef96fb0 (patch) | |
| tree | 1479c5e61cb174356bc5deea2f6ec64b05f21036 /kernel/nativelibrary.mli | |
| parent | 45306c6c9c433b86406d041f58aafb7cf3a3ff82 (diff) | |
Move type definition Nativecode.symbols to Nativevalues
Preparing for it to be stored in an Environ.env.
Diffstat (limited to 'kernel/nativelibrary.mli')
| -rw-r--r-- | kernel/nativelibrary.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/nativelibrary.mli b/kernel/nativelibrary.mli index 31e5255fc4..1485e97b47 100644 --- a/kernel/nativelibrary.mli +++ b/kernel/nativelibrary.mli @@ -16,4 +16,4 @@ open Nativecode compiler *) val dump_library : ModPath.t -> DirPath.t -> env -> module_signature -> - global list * symbols + global list * Nativevalues.symbols |