diff options
| author | Jean-Christophe Filliatre | 2014-10-25 21:12:50 +0200 |
|---|---|---|
| committer | Jean-Christophe Filliatre | 2014-10-25 21:13:01 +0200 |
| commit | 0397aa549645df23cc50c9018b543e6c0b346d62 (patch) | |
| tree | 3f0a175c5057126511433aa7d8c8d893db8b4eab /kernel/type_errors.mli | |
| parent | bf018569405c0ae1c5d08dfa27600102b9d77977 (diff) | |
Changed implementation of lib/heap.ml to use Braun trees
The previous implementation was embarrassingly naive and inefficient.
For elements with the same priority, this new implementation may return
a maximum element that is different (yet still with the highest priority,
of course).
This code is used only in tactic firstorder.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions