summaryrefslogtreecommitdiff
path: root/doc/README
diff options
context:
space:
mode:
Diffstat (limited to 'doc/README')
-rwxr-xr-xdoc/README30
1 files changed, 0 insertions, 30 deletions
diff --git a/doc/README b/doc/README
deleted file mode 100755
index 14cb6e44..00000000
--- 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).