This is a development of treesort. The main file is {\tt Heap.v}.  A
Caml-Light program {\tt treesort.ml} can be automatically extracted
from the proof (see the description of the {\tt Extraction} tactic in
the additional document \verb!Extraction.dvi!).
