coq _unstable_ port information

Package: coq
Version: 8.2pl1
Revision: 1
Source: http://coq.inria.fr/distrib/V%v/files/coq-%v.tar.gz
Source-MD5: 36eed48bc63ada8abf27f96eb126906c
Maintainer: Bruno De Fraine
HomePage: http://coq.inria.fr/
License: LGPL
Description: Proof assistant for higher-order logic
BuildDepends: fink (>= 0.24.12), ocaml (>=3.10), camlp5
Recommends: coq-dev
Suggests: coq-doc, coqide
PatchFile: %n.patch
PatchFile-MD5: e11f5ec8d34d76457a45134a07149f0a
CompileScript: <<
./configure -prefix %p -coqdocdir %p/share/doc/coq -mandir %p/share/man -emacslib %p/share/emacs/site-lisp/coq -opt -reals all -browser 'open %%s'
make revision coq
make -f Makefile.stage3 doc/stdlib/html/index.html
<<
InstallScript: <<
make install-coq COQINSTALLPREFIX=%d
mkdir -p %i/share/doc/%n/stdlib
cp -r doc/stdlib/html %i/share/doc/%n/stdlib
cp tools/coqdoc/coqdoc.css %i/share/doc/%n/stdlib/html
<<
DocFiles: CHANGES COPYRIGHT CREDITS LICENSE README README.fink
SplitOff: <<
Package: coq-dev
Description: Material for developing Coq user tactics
Depends: coq (=%v-%r), ocaml (>=3.10), camlp5
Files: bin/coqmktop share/man/man1/coqmktop.1 lib/coq/config lib/coq/lib lib/coq/kernel lib/coq/library lib/coq/pretyping lib/coq/interp lib/coq/proofs lib/coq/parsing lib/coq/tactics lib/coq/toplevel lib/coq/contrib/contrib.*
<<
DescDetail: <<
Developed in the LogiCal project (http://logical.inria.fr),
the Coq tool is a formal proof management system: a proof done with
Coq is mechanically checked by the machine.

In particular, Coq allows one:
* to define functions and predicates
* to state mathematical theorems and software specifications
* to develop interactively formal proofs of these theorems
* to check these proofs by a small certification "kernel".

Coq is based on a logical framework called "Calculus of Inductive
Constructions" extended by a modular development system for
theories.

Coq also includes
* a mecanism to automatically generate certified programs
* proofs of the specifications of these programs
* a documentation tool (coqdoc)
* dependecy and makefile generation tools for Coq
* a preprocessor for TeX files that include Coq commands (coq-tex)

This package provides the core coq tools, together with documentation for
the standard library; the files to build custom tactics in Ocaml are
available in `coq-dev'; the reference manual and some other documentation is
available in the `coq-doc' package; a graphical user environment is
contained in the `coqide' package.
<<