aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativecode.ml
diff options
context:
space:
mode:
authorMatej Kosik2016-06-20 15:08:11 +0200
committerMatej Kosik2016-06-20 15:10:39 +0200
commit0fa8b96c243e0915477866b094735ecaaaac6ef6 (patch)
tree9e9b4d046a087b1dbf9684611338bf29a5fdd6b7 /kernel/nativecode.ml
parentc064fb933a16dc25b8172a1a2e758f538ee7285e (diff)
Reference Manual / Extraction: the original example command no longer works with recent Coq
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions