Mise à jour des fichiers README et INSTALL de la doc (bug #1921) + suppression de la dépendance envers aeguill (bug #1922)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11311 85f007b7-540e-0410-9357-904b9bb8a0f7

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}