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 package provides runtime libraries for coq.