aboutsummaryrefslogtreecommitdiff
path: root/academic/coq/README
diff options
context:
space:
mode:
Diffstat (limited to 'academic/coq/README')
-rw-r--r--academic/coq/README9
1 files changed, 2 insertions, 7 deletions
diff --git a/academic/coq/README b/academic/coq/README
index eec7b1118a2b6..81ec48f0d65e7 100644
--- a/academic/coq/README
+++ b/academic/coq/README
@@ -3,13 +3,8 @@ language called Gallina that is based on an expressive formal language
called the Calculus of Inductive Constructions that itself combines both
a higher-order logic and a richly-typed functional programming language.
-This requires OCaml (>= 3.10.2), camlp5 (with "transitional mode", avoiding
-version 5.0.0), and GNU Make (>= 3.81). If you have ocamlopt, Coq
-will be compiled to native code, which runs 4-10 times faster. For best
-performance, OCaml should have support for pthreads.
-
-Note: camlp5 6.01 appears to have a bug that prevents Coq from building
-correctly. This build has been tested with 6.02.3.
+If you have ocamlopt, Coq will be compiled to native code, which runs 4-10
+times faster. For best performance, OCaml should have support for pthreads.
If you want CoqIDE, you need LablGTK2 (>= 2.10.0) with development
files, and GTK2+ (>= 2.10.0). This also REQUIRES OCaml to have support