aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativelib.ml
diff options
context:
space:
mode:
authorJasper Hugunin2020-09-12 21:03:31 -0700
committerJasper Hugunin2020-09-16 13:23:13 -0700
commitcc4494897f0897f5795c2bd25fc06d4b07c73667 (patch)
tree596ed5ed585ee2cf9acf6ba2a8af26faa7a0d5ba /kernel/nativelib.ml
parent862a5b352e784fff9f1a9bde5ac3b887403ece57 (diff)
Modify setoid_ring/BinList.v to compile with -mangle-names
Diffstat (limited to 'kernel/nativelib.ml')
0 files changed, 0 insertions, 0 deletions