diff options
| -rw-r--r-- | academic/coq/README | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/academic/coq/README b/academic/coq/README index eec7b1118a..81ec48f0d6 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 |