diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-04-02 02:11:59 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-04-09 22:00:20 +0200 |
commit | 9aa27e4554c607ea9bd94c999bf828c2874cf22a (patch) | |
tree | d8896f21902a674257d34639c708bc85d0bae3fa /theories/ZArith/Zmax.v | |
parent | ba636891121821b4943a0464b49e14de54de8253 (diff) |
Fix an algorithmic issue in Nsatz.
We use heaps instead of continuously adding elements to an ordered list,
which was quadratic in the worst case.
As a byproduct, this solves bug #5359, which was due to a stack overflow on
big lists.
Diffstat (limited to 'theories/ZArith/Zmax.v')
0 files changed, 0 insertions, 0 deletions