diff options
| author | Pierre-Marie Pédrot | 2020-07-22 15:06:35 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-07-25 16:58:53 +0200 |
| commit | b4bc3b747abf4840cc29b8e478cbe36ebaeaded1 (patch) | |
| tree | eb95f12da8abe24cd6fabfd089659d311da5b3c8 /tools/TimeFileMaker.py | |
| parent | 55f4095fe3c366a9f310584a55e2dc0605e5409c (diff) | |
Faster algorithm to compute algebraic universe mapping in mimization.
Instead of crawling a map in O(n) we preserve a backwards map at the same time.
This inefficiency was observed in coq-performance-tests/n_polymorphic_universes.v.
Diffstat (limited to 'tools/TimeFileMaker.py')
0 files changed, 0 insertions, 0 deletions