aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativecode.mli
diff options
context:
space:
mode:
authorMaxime Dénès2017-04-11 18:37:31 +0200
committerMaxime Dénès2017-04-11 18:37:31 +0200
commitf41944730792070d4a3074aa1fe1f8465062b758 (patch)
treec550529678e91bb15096f862f9a61a1931b2d608 /kernel/nativecode.mli
parentb5155a6690c9c768182cbedac9d6f61d11df2965 (diff)
parentaa704399c4d4b8a74f4d6f42e65808c1ceab3b7e (diff)
Merge PR#549: Fast path in weak head reduction of applied atoms.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions