Brief description of the package:
Theorem prover which extracts programs from proofs
Please read the file "DESCR" for a longer description, or browse the package's history.
This package has a home page at http://coq.inria.fr/.
The package is located in the "lang/coq" directory. The current source version of the package is "coq-8.1pl3nb1". For a summary on how to use the package collection, go to the top of the packages tree.
Problem reports, updates or suggestions for this package should be reported with send-pr.
The following security vulnerabilities are known for lang/coq :
This package requires the following package(s) to build: camlp5>=5.01 ocaml>=3.08.2 gmake>=3.81 ocaml>=3.09.1nb2 ocaml>=3.09 .
This package requires the following package(s) to run: camlp5>=5.01 .
Select one of the links below to download the package in precompiled binary form for installation with pkg_add(1). Available machine architectures and package versions:
| i386: | coq-8.1pl2.tgz | (NetBSD 4.0) |
| powerpc: | coq-8.0pl2.tgz | (Darwin 8.1.0) |
| powerpc: | coq-8.1.tgz | (NetBSD 4.0_BETA2) |
| sparc: | coq-8.1.tgz | (NetBSD 2.1) |
| sparc: | coq-8.1.tgz | (NetBSD 2.1) |
| x86_64: | coq-8.1pl3nb1.tgz | (NetBSD 4.99.62) |
The NetBSD packages collection is designed to permit easy installation from source - particularly useful if the latest binary package is not available for your chosen platform.