From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 28 Apr 2006 14:59:16 +0000 Subject: Imported Upstream version 8.0pl3+8.1alpha --- doc/README | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) create mode 100755 doc/README (limited to 'doc/README') diff --git a/doc/README b/doc/README new file mode 100755 index 00000000..14cb6e44 --- /dev/null +++ b/doc/README @@ -0,0 +1,30 @@ +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). -- cgit v1.2.3