diff options
| author | Hugo Herbelin | 2016-03-28 09:15:08 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-06-10 02:44:34 +0200 |
| commit | 611db91aed4ca748ac7effaf0024ba6d0d102810 (patch) | |
| tree | 57aab63db274c59522b5bc4f2268f41e4fa1dec1 /kernel | |
| parent | 7527751d9772656b4680df311546825cc2dd3d8f (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')
0 files changed, 0 insertions, 0 deletions