Compact data structures in Coq

This is a pre-release whose main purpose is to test a forthcoming opam package. It is however already axiom-free and documented by research manuscripts.