diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-05-09 15:51:15 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-05-10 19:23:55 +0200 |
| commit | 0e271d68a5bc6f5b8bc9a4ed2b9cf2faf283397e (patch) | |
| tree | 0f77f8f53a767dc184afd129bb3b27c0ac27a425 /doc | |
| parent | faa22df091613de7cb1b91ed7f64e5fed6fae812 (diff) | |
Suggest going to /documentation to see a list of tutorials.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/biblio.bib | 9 | ||||
| -rw-r--r-- | doc/sphinx/introduction.rst | 11 |
2 files changed, 5 insertions, 15 deletions
diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib index 97231c9ec..aeb45611e 100644 --- a/doc/sphinx/biblio.bib +++ b/doc/sphinx/biblio.bib @@ -1201,15 +1201,6 @@ Decomposition}}, note = {\url{https://proofgeneral.github.io/}} } -@Book{CoqArt, - title = {Interactive Theorem Proving and Program Development. - Coq'Art: The Calculus of Inductive Constructions}, - author = {Yves Bertot and Pierre Castéran}, - publisher = {Springer Verlag}, - series = {Texts in Theoretical Computer Science. An EATCS series}, - year = 2004 -} - @InCollection{wadler87, author = {P. Wadler}, title = {Efficient Compilation of Pattern Matching}, diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst index 4a313df0c..75ff72c4d 100644 --- a/doc/sphinx/introduction.rst +++ b/doc/sphinx/introduction.rst @@ -2,12 +2,11 @@ Introduction ------------------------ -This document is the Reference Manual of the |Coq| proof -assistant. A companion volume, the |Coq| Tutorial, is provided for the -beginners. It is advised to read the Tutorial first. A -book :cite:`CoqArt` on practical uses of the |Coq| system was -published in 2004 and is a good support for both the beginner and the -advanced user. +This document is the Reference Manual of the |Coq| proof assistant. +To start using Coq, it is advised to first read a tutorial. +Links to several tutorials can be found at +https://coq.inria.fr/documentation (see also +https://github.com/coq/coq/wiki#coq-tutorials). The |Coq| system is designed to develop mathematical proofs, and especially to write formal specifications, programs and to verify that |