Fix a line in Ocaml code which was broken at the wrong place.
Various updates suggested by the reviewers.
A small improvement in the Coq code.