diff options
| author | Matthieu Sozeau | 2013-11-14 16:20:09 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-06 09:58:56 +0200 |
| commit | 021d5dbac4ce3cd89e6ac87ec3ca0687d4fdfd10 (patch) | |
| tree | 22b4086fa771f477fe1b9c31cbd000689a4d5d49 /lib | |
| parent | d89e1efccd0bc59142db53a4f808fb09d1e84bf5 (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 'lib')
0 files changed, 0 insertions, 0 deletions