aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativecode.mli
diff options
context:
space:
mode:
authorHugo Herbelin2016-03-28 09:15:08 +0200
committerHugo Herbelin2016-06-10 02:44:34 +0200
commit611db91aed4ca748ac7effaf0024ba6d0d102810 (patch)
tree57aab63db274c59522b5bc4f2268f41e4fa1dec1 /kernel/nativecode.mli
parent7527751d9772656b4680df311546825cc2dd3d8f (diff)
A mini-optimization for free in unification.ml: test in O(1)
complexity comes before tests in O(n) complexity.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions