coq-doc _unstable_ port information

Package: coq-doc
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: OSI-Approved
DocFiles: doc/LICENSE README.doc README.fink
PatchFile: %n.patch
PatchFile-MD5: 5b12af6a2f435e9f6e0d20c122a074b6
Description: Additional PDF and HTML documentation for Coq
BuildDepends: fink (>= 0.24.12), coq (= %v-%r), tetex-base, tetex-texmf, hevea, netpbm-bin
Recommends: coq
CompileScript: <<
make -f Makefile.common -f Makefile.doc QUICK=1 COQSRC=%p VERSION=%v COQTEXOPTS="-sl -small" refman tutorial faq rectutorial
<<
InstallScript: <<
mkdir -p %i/share/doc/coq
cp doc/tutorial/Tutorial.v.html %i/share/doc/coq/Tutorial.html
cp doc/tutorial/Tutorial.v.pdf %i/share/doc/coq/Tutorial.pdf
cp doc/RecTutorial/RecTutorial.html %i/share/doc/coq/RecTutorial.html
cp doc/RecTutorial/RecTutorial.pdf %i/share/doc/coq/RecTutorial.pdf
mkdir -p %i/share/doc/coq/refman
cp -r doc/refman/html %i/share/doc/coq/refman/
chmod -R o+rX %i/share/doc/coq/refman
cp doc/refman/Reference-Manual.pdf %i/share/doc/coq/refman/
mkdir -p %i/share/doc/coq/faq
cp -r doc/faq/html %i/share/doc/coq/faq/
chmod -R o+rX %i/share/doc/coq/faq
cp doc/faq/FAQ.v.pdf %i/share/doc/coq/faq/FAQ.pdf
<<
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 for automatically generating 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 additional HTML and PDF documentation for
Coq. The documentation consists of
* The Tutorial
* The Reference manual
* FAQ about Coq
* A Tutorial on Recursive Types in Coq
<<