SlackBuildsOrg/academic/coq
dsomero d0c108251a various: Update find command to match template.
Signed-off-by: dsomero <xgizzmo@slackbuilds.org>
2013-11-22 02:37:19 -05:00
..
coq.info *: newest dep-fixes 2012-09-01 18:38:43 +02:00
coq.SlackBuild various: Update find command to match template. 2013-11-22 02:37:19 -05:00
gpl.txt.gz academic/coq: Added (The Coq Proof Assistant) 2011-08-05 11:11:34 -03:00
README academic/coq: Fixed dep information 2012-08-22 16:07:13 -05:00
slack-desc various: Fix slack-desc formatting and comment nit picks. 2013-11-22 02:29:22 -05:00

Coq implements a program specification and mathematical higher-level
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.

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
for pthreads.

If you have emacs installed, emacs files for Coq will be installed.
Otherwise, they will be omitted.