I am coming here from the Coq mailing list, because of a link posted there
about this e-mail thread.  I have been working on Coq-verified and fully
proof-erased versions of AVL and red-black trees, as well as a variant I
didn't know existed before, until I read about "2-imbalance AVL trees" in this
thread.

The github address for my development is:

https://github.com/jonleivent/mindless-coding

and the "gaptree" development there may be the same as your "2-imbalance" AVL
trees, though I can't be sure without more of an explanation (or maybe just a
pointer to the source code) for the 2-imbalance AVL trees.

Any further information or source pointers you can give me would be greatly
appreciated.

Thanks
--Jonathan

--
Caml-list mailing list.  Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs