Initial revision

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

1 files changed, 45 insertions, 0 deletions

diff --git a/doc/README b/doc/README
new file mode 100755
index 0000000000..832e6167c0
--- /dev/null
+++ b/doc/README
@@ -0,0 +1,45 @@
+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
+V6.3.1 is divided into the following documents :
+
+     * Tutorial.ps: An introduction to the use of the Coq Proof Assistant;
+
+     * Reference-Manual-base.ps:  215 pp., includes
+
+     - the description of Gallina, the language of Coq
+     - the description of the Vernacular, the commands of Coq
+     - the description of each tactic
+     - chapters about Grammar/Syntax extentions and Writing tactics
+     - index on tactics, commands and error messages
+
+     * Reference-Manual-addendum.ps, 75 pp., includes more detailed
+      explanations and examples about the following topics:
+
+     - the extended Cases (C.Cornes)
+     - the Coercions (A. Saïbi)
+     - the tactic Omega (P. Crégut)
+     - printing proofs in natural language (Y. Coscoy)
+     - the tactic Ring (S. Boutin and P. Loiseleur)
+     - the Program tactic (C. Parent)
+     - the Correctness tactic (J.-C. Filliâtre)
+     - the extraction features (J.-C. Filliâtre)
+
+     Index, page and chapter numbers are shared by the two documents, in
+     order to make cross-references possible. There is also a on the ftp
+     server a Postscript file Reference-Manual-all.ps that contains the two
+     documents (base and addendum).
+
+     * Library.ps: A description of the Coq standard library;
+
+     * Changes.ps: A description of the differences between the
+       versions V6.3 and V6.3.1;
+
+     * rectypes.ps : A tutorial on recursive types by Eduardo Gimenez
+
+Documentation is also available in the DVI format (you can get the DVI docs 
+separately or in the tar file all-dvi.docs.tar).
+
+The Reference Manual and the Tutorial are also available in HTML format 
+(online at http://coq.inria.fr or by ftp in the file doc-html.tar.gz).
+