diff options
author | Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
commit | 870075f34dd9fa5792bfbf413afd3b96f17e76a0 (patch) | |
tree | 0c647056de1832cf1dba5ba58758b9121418e4be /doc | |
parent | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (diff) |
Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg
Diffstat (limited to 'doc')
-rw-r--r-- | doc/INSTALL | 65 | ||||
-rw-r--r-- | doc/LICENSE (renamed from doc/LICENCE) | 0 | ||||
-rwxr-xr-x | doc/README | 30 |
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). |