diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-05-11 15:03:43 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-05-11 15:03:43 +0200 |
| commit | 83b2e3430da9ba6d234a78c5b2910070c13d4152 (patch) | |
| tree | 70004f9c65488a3cf4da850fcb1098547b872ade /doc/sphinx | |
| parent | c3d719caf951e0c3716c85c8e3cf45f636d059eb (diff) | |
| parent | 0e271d68a5bc6f5b8bc9a4ed2b9cf2faf283397e (diff) | |
Merge PR #7466: Remove tutorials from the repo
Diffstat (limited to 'doc/sphinx')
| -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 |