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 Camlp4. For more information, see . . This package provides existing theories that new proofs can be based upon, including theories of arithmetic and Boolean values.