aboutsummaryrefslogtreecommitdiff
path: root/kernel/constr.mli
diff options
context:
space:
mode:
authorMatthieu Sozeau2013-11-14 16:20:09 +0100
committerMatthieu Sozeau2014-05-06 09:58:56 +0200
commit021d5dbac4ce3cd89e6ac87ec3ca0687d4fdfd10 (patch)
tree22b4086fa771f477fe1b9c31cbd000689a4d5d49 /kernel/constr.mli
parentd89e1efccd0bc59142db53a4f808fb09d1e84bf5 (diff)
In kernel/univ.ml, better allocation behavior, better eq_univs function
avoiding doing work twice, better leq not duplicating a Universe.equal test. Conflicts: kernel/univ.ml
Diffstat (limited to 'kernel/constr.mli')
0 files changed, 0 insertions, 0 deletions