diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2013-11-12 19:19:13 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:58:55 +0200 |
| commit | 28e5f4def8bebdaf3bd75b6662bbd4fd88594689 (patch) | |
| tree | 3f4dd3966b7be0ade898b6fceb055918e76f8ae1 /lib/bigint.mli | |
| parent | de1f3069045e5b21804b9f58a3510999ef580c84 (diff) | |
Better hashconsing of levels and universes, working with modules.
Huge slowdown to be tracked in some files, even if no polymorphism is
involved.
Conflicts:
kernel/univ.ml
Diffstat (limited to 'lib/bigint.mli')
0 files changed, 0 insertions, 0 deletions