Proof assistant for higher-order logic

Current versions

coq requires the following formulae to be installed:
ocaml-findlib 1.7.3 OCaml library manager
camlp5 7.05 Preprocessor and pretty-printer for OCaml
ocaml 4.06.1 General purpose programming language in the ML family
ocaml-num 1.1_2 OCaml legacy Num library for arbitrary-precision arithmetic

Reverse dependencies

The following formula requires coq to be installed:
compcert 3.2 Formally verified C compiler

Recent formula history

ilovezfs coq 8.7.2
ilovezfs coq 8.7.1
ilovezfs coq: depend on ocaml-num
ilovezfs Use “squiggly” heredocs.
ilovezfs coq 8.7.0

Formula code at GitHub