diff options
| author | Hugo Herbelin | 2018-10-29 11:27:15 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-10-31 16:16:41 +0100 |
| commit | d1091555104e0198eaaa94a1bb69e96d5cc73447 (patch) | |
| tree | dd5f0704a368604e27944c48b1a735c9ab4a8369 /kernel/nativevalues.ml | |
| parent | ae39925d64cc51663ab3f2ad397501b435bd0e5e (diff) | |
Seeing Global purely as a wrapper on top of kernel functions.
Diffstat (limited to 'kernel/nativevalues.ml')
0 files changed, 0 insertions, 0 deletions