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/nativelib.ml | |
| parent | 45306c6c9c433b86406d041f58aafb7cf3a3ff82 (diff) | |
Move type definition Nativecode.symbols to Nativevalues
Preparing for it to be stored in an Environ.env.
Diffstat (limited to 'kernel/nativelib.ml')
0 files changed, 0 insertions, 0 deletions