From 738fcf4d628ac0910d21ebbee498fb9e490eea85 Mon Sep 17 00:00:00 2001 From: Robby Workman Date: Tue, 21 Aug 2012 20:28:50 -0500 Subject: academic/coq: Fixed dep information Signed-off-by: Robby Workman --- academic/coq/README | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) (limited to 'academic/coq/README') 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 -- cgit v1.2.3