aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coq_makefile.ml
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-03-28 09:15:08 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-06-10 02:44:34 +0200
commit611db91aed4ca748ac7effaf0024ba6d0d102810 (patch)
tree57aab63db274c59522b5bc4f2268f41e4fa1dec1 /tools/coq_makefile.ml
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 'tools/coq_makefile.ml')
0 files changed, 0 insertions, 0 deletions