------------------------------------------------------------------------------ Organisation of the sub-directories: TLC/ Charguéraud's general-purpose Coq library. CFML/ Charguéraud's CFML tool and Coq library. vocal/src/ OCaml source code, including HashTable.{ml,mli}. vocal/proofs/ vocal/proofs/Cascade vocal/proofs/HashTable Proofs about the OCaml source code. ------------------------------------------------------------------------------