diff options
-rw-r--r-- | INSTALL.doc (renamed from doc/INSTALL) | 50 | ||||
-rwxr-xr-x | README.doc | 18 | ||||
-rw-r--r-- | doc/LICENSE (renamed from doc/LICENCE) | 0 | ||||
-rwxr-xr-x | doc/README | 30 | ||||
-rw-r--r-- | doc/RecTutorial/RecTutorial.tex | 24 |
5 files changed, 63 insertions, 59 deletions
diff --git a/doc/INSTALL b/INSTALL.doc index 9223a41bd..3eb72e08b 100644 --- a/doc/INSTALL +++ b/INSTALL.doc @@ -15,12 +15,7 @@ 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 +To produce the PostScript documents, the following tools are needed: - latex (latex2e) @@ -38,26 +33,47 @@ 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 +To produce all documentation about Coq, just run: + + make doc + + +Alternatively, you can use some specific targets: + + make doc-ps + to produce all PostScript documents + + make doc-pdf + to produce all PDF documents + + make doc-html + to produce all html documents + + make refman + to produce all formats of the reference manual + + make tutorial + to produce all formats of the tutorial + + make rectutorial + to produce all formats of the tutorial on recursive types + + make faq + to produce all formats of the FAQ + + make stdlib + to produce all formats of the Coq standard library + Installation ------------ To install all produced documents, do: - make DOCDIR=/some/directory/for/documentation install + make DOCDIR=/some/directory/for/documentation install-doc DOCDIR defauts to /usr/share/doc/coq-x.y were x.y is the version number diff --git a/README.doc b/README.doc new file mode 100755 index 000000000..4e72c894b --- /dev/null +++ b/README.doc @@ -0,0 +1,18 @@ + The Coq documentation + ===================== + +The Coq documentation includes: + +- a reference manual; +- a generic tutorial on Coq; +- a tutorial on recursive types; +- a document presenting the Coq standard library; +- a list of questions/answers in the FAQ style + +All these documents are available online from the Coq official site +(http://coq.inria.fr), either as PS/PDF files or as HTML documents. + +The sources of the documentation are available along with the sources +of the Coq proof assistant. It is released under the Open Publication +License (see file doc/LICENSE in the sources of Coq) + diff --git a/doc/LICENCE b/doc/LICENSE index 990874803..990874803 100644 --- a/doc/LICENCE +++ b/doc/LICENSE diff --git a/doc/README b/doc/README deleted file mode 100755 index 14cb6e448..000000000 --- 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). diff --git a/doc/RecTutorial/RecTutorial.tex b/doc/RecTutorial/RecTutorial.tex index df8bc9f10..56c4f172a 100644 --- a/doc/RecTutorial/RecTutorial.tex +++ b/doc/RecTutorial/RecTutorial.tex @@ -5,24 +5,24 @@ Pierre Cast\'eran\thanks{Pierre.Casteran@labri.fr}} \date{May 1998 --- \today} \usepackage{multirow} -\usepackage{aeguill} -%\externaldocument{RefMan-gal.v} -%\externaldocument{RefMan-ext.v} -%\externaldocument{RefMan-tac.v} -%\externaldocument{RefMan-oth} -%\externaldocument{RefMan-tus.v} -%\externaldocument{RefMan-syn.v} -%\externaldocument{Extraction.v} +% \usepackage{aeguill} +% \externaldocument{RefMan-gal.v} +% \externaldocument{RefMan-ext.v} +% \externaldocument{RefMan-tac.v} +% \externaldocument{RefMan-oth} +% \externaldocument{RefMan-tus.v} +% \externaldocument{RefMan-syn.v} +% \externaldocument{Extraction.v} \input{recmacros} \input{coqartmacros} \newcommand{\refmancite}[1]{{}} -%\newcommand{\refmancite}[1]{\cite{coqrefman}} -%\newcommand{\refmancite}[1]{\cite[#1] {]{coqrefman}} +% \newcommand{\refmancite}[1]{\cite{coqrefman}} +% \newcommand{\refmancite}[1]{\cite[#1] {]{coqrefman}} \usepackage[latin1]{inputenc} \usepackage[T1]{fontenc} \usepackage{makeidx} -%\usepackage{multind} +% \usepackage{multind} \usepackage{alltt} \usepackage{verbatim} \usepackage{amssymb} @@ -31,7 +31,7 @@ Pierre Cast\'eran\thanks{Pierre.Casteran@labri.fr}} \usepackage[dvips]{epsfig} \usepackage{epic} \usepackage{eepic} -\usepackage{ecltree} +% \usepackage{ecltree} \usepackage{moreverb} \usepackage{color} \usepackage{pifont} |