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.