summaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2008-08-08 13:18:42 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2008-08-08 13:18:42 +0200
commit870075f34dd9fa5792bfbf413afd3b96f17e76a0 (patch)
tree0c647056de1832cf1dba5ba58758b9121418e4be /doc
parenta0cfa4f118023d35b767a999d5a2ac4b082857b4 (diff)
Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg
Diffstat (limited to 'doc')
-rw-r--r--doc/INSTALL65
-rw-r--r--doc/LICENSE (renamed from doc/LICENCE)0
-rwxr-xr-xdoc/README30
3 files changed, 0 insertions, 95 deletions
diff --git a/doc/INSTALL b/doc/INSTALL
deleted file mode 100644
index 9223a41b..00000000
--- a/doc/INSTALL
+++ /dev/null
@@ -1,65 +0,0 @@
- The Coq documentation
- =====================
-
-The Coq documentation includes
-
-- A Reference Manual
-- A Tutorial
-- A document presenting the Coq standard library
-- A list of questions/answers in the FAQ style
-
-The sources of the documents are mainly made of LaTeX code from which
-user-readable PostScript or PDF files, or a user-browsable bunch of
-html files are generated.
-
-Prerequisite
-------------
-
-To produce the documents, you need the coqtop, coq-tex, coqdoc and
-gallina tools, with same version number as the current
-documentation. These four tools normally come with any basic Coq
-installation.
-
-In addition, to produce the PostScript documents, the following tools
-are needed:
-
- - latex (latex2e)
- - dvips
- - bibtex
- - makeindex
- - pngtopnm and pnmtops (for the Reference Manual and the FAQ)
-
-To produce the PDF documents, the following tools are needed:
-
- - pdflatex
- - bibtex
-
-To produce the html documents, the following tools are needed:
-
- - hevea (e.g. 1.07 works)
-
-To produce the documentation of the standard library, a source copy of
-the coq distribution is needed.
-
-Compilation
------------
-
-To produce all PostScript documents, do: make all-ps
-To produce all PDF documents, do: make all-pdf
-To produce all html documents, do: make all-html
-To produce all formats of the Reference Manual, do: make refman
-To produce all formats of the Tutorial, do: make tutorial
-To produce all formats of the Coq Standard Library, do: make stdlib
-To produce all formats of the FAQ, do: make faq
-
-Installation
-------------
-
-To install all produced documents, do:
-
- make DOCDIR=/some/directory/for/documentation install
-
-DOCDIR defauts to /usr/share/doc/coq-x.y were x.y is the version number
-
-
-
diff --git a/doc/LICENCE b/doc/LICENSE
index 99087480..99087480 100644
--- a/doc/LICENCE
+++ b/doc/LICENSE
diff --git a/doc/README b/doc/README
deleted file mode 100755
index 14cb6e44..00000000
--- a/doc/README
+++ /dev/null
@@ -1,30 +0,0 @@
-You can get the whole documentation of Coq in the tar file all-ps-docs.tar.
-
-You can also get separately each document. The documentation of Coq
-V8.0 is divided into the following documents :
-
- * Tutorial.ps: An introduction to the use of the Coq Proof Assistant;
-
- * Reference-Manual.ps:
-
- Base chapters:
- - the description of Gallina, the language of Coq
- - the description of the Vernacular, the commands of Coq
- - the description of each tactic
- - index on tactics, commands and error messages
-
- Additional chapters:
- - the extended Cases (C.Cornes)
- - the coercions (A. Saïbi)
- - the tactic Omega (P. Crégut)
- - the extraction features (J.-C. Filliâtre and P. Letouzey)
- - the tactic Ring (S. Boutin and P. Loiseleur)
- - the Setoid_replace tactic (C. Renard)
- - etc.
-
- * Library.ps: A description of the Coq standard library;
-
- * rectypes.ps : A tutorial on recursive types by Eduardo Gimenez
-
-Documentation is also available in the PDF format and HTML format
-(online at http://coq.inria.fr or by ftp in the file doc-html.tar.gz).