sci-mathematics/coq
Coq is a proof assistant written in O'Caml
Screenshots
View
DownloadUSE Flags
norealanalysis
Global: Do not build real analysis modules (faster compilation)
Local: Do not build real analysis modules (faster compilation)
ide
Global: Enable the qsa ide
Local: Build the Coq IDE, a clone of proof general using dev-ml/lablgtk
debug
Global: Enable extra debug codepaths, like asserts and extra output. If you want to get meaningful backtraces see http://www.gentoo.org/proj/en/qa/backtraces.xml
+ocamlopt
Global: