aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativecode.ml
diff options
context:
space:
mode:
authorHugo Herbelin2017-03-03 14:43:00 +0100
committerHugo Herbelin2017-03-03 14:44:42 +0100
commit9133d6faece4feb675fdc9c66cebcb2bba9246a9 (patch)
treefb5ef56768e88e111fa39c88f3ef791be4d728fa /kernel/nativecode.ml
parent620f1918452b898d6663cabb5e0f341c7e767017 (diff)
CHANGES: choice over setoids and prop. ext.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions