Coq is a proof assistant for higher-order logic, which allows the development of computer programs consistent with their formal specification. it is developed using objective caml and camlp5.

this is a dummy package which will install the documentation in html and pdf formats.