Skip to content


Subversion checkout URL

You can clone with
Download ZIP
Browse files

Mise à jour des fichiers README et INSTALL de la doc (bug #1921) + su…

…ppression de la dépendance envers aeguill (bug #1922)

git-svn-id: svn+ssh:// 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information...
commit 2592766937df60484f15d5050e5bfe6623c83390 1 parent 99ceb8c
notin authored
50 doc/INSTALL → INSTALL.doc
@@ -15,12 +15,7 @@ html files are generated.
-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
-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.
-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
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
18 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
+(, 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)
0  doc/LICENCE → doc/LICENSE
File renamed without changes
30 doc/README
@@ -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 :
- * An introduction to the use of the Coq Proof Assistant;
- *
- 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.
- * A description of the Coq standard library;
- * : A tutorial on recursive types by Eduardo Gimenez
-Documentation is also available in the PDF format and HTML format
-(online at or by ftp in the file doc-html.tar.gz).
24 doc/RecTutorial/RecTutorial.tex
@@ -5,24 +5,24 @@
\date{May 1998 --- \today}
+% \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}
-%\newcommand{\refmancite}[1]{\cite[#1] {]{coqrefman}}
+% \newcommand{\refmancite}[1]{\cite{coqrefman}}
+% \newcommand{\refmancite}[1]{\cite[#1] {]{coqrefman}}
+% \usepackage{multind}
@@ -31,7 +31,7 @@
+% \usepackage{ecltree}
Please sign in to comment.
Something went wrong with that request. Please try again.