aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativelib.ml
diff options
context:
space:
mode:
authorGuillaume Melquiond2021-02-19 19:29:46 +0100
committerGuillaume Melquiond2021-02-19 19:29:46 +0100
commit21ed2bfa901108d69893bc8480d215edeb255d6d (patch)
tree19c88c13d9400ddc03e76a3dd0200503e456d128 /kernel/nativelib.ml
parent88e688182ded232f474102d400e4e4e95861f94d (diff)
Abstract the non-computational part away.
Diffstat (limited to 'kernel/nativelib.ml')
0 files changed, 0 insertions, 0 deletions