aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativecode.ml
diff options
context:
space:
mode:
authorAmin Timany2017-05-24 13:45:08 +0200
committerEmilio Jesus Gallego Arias2017-06-16 04:51:18 +0200
commitc01d225f9e112bb08f9df26f70805bde0c0d127a (patch)
tree793f803d3fa99bb480e3312960266d038381513f /kernel/nativecode.ml
parente28d3a488c81c6dc59aa8f53d98a95ee93a84d37 (diff)
Enable the checking of ind subtyping in checker
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions