Typo.
Full.v: PowerList.of_blist_with_cast -> of_binary_list.
First version of the Coq section.
Coq & Ocaml modes: vertical bars connect in match, and type definitions.