• Jean-Christophe Filliatre's avatar
    library: several changes in pqueue · 309be35d
    Jean-Christophe Filliatre authored
    - both Pqueue and PqueueNoDup now require a TotalPreOrder, not TotalOrder
    - Pqueue now modeled using sequences instead of lists
    - a harness module for Pqueue (external heapsort)
    - both Pqueue and PqueueNoDup now have coercions
To find the state of this project's repository at the time of any of these versions, check out the tags.