diff options
| author | notin | 2008-08-06 15:34:14 +0000 |
|---|---|---|
| committer | notin | 2008-08-06 15:34:14 +0000 |
| commit | 2592766937df60484f15d5050e5bfe6623c83390 (patch) | |
| tree | eb5c6f7437882f4c85b7b4ca1d340644f426e02f /doc/README | |
| parent | 99ceb8c7df67a37330820e3e6fbb4a3ccab2a9a5 (diff) | |
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
Diffstat (limited to 'doc/README')
| -rwxr-xr-x | doc/README | 30 |
1 files changed, 0 insertions, 30 deletions
diff --git a/doc/README b/doc/README deleted file mode 100755 index 14cb6e448b..0000000000 --- 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). |
