From 0e271d68a5bc6f5b8bc9a4ed2b9cf2faf283397e Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 9 May 2018 15:51:15 +0200 Subject: Suggest going to /documentation to see a list of tutorials. --- doc/sphinx/biblio.bib | 9 --------- 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 97231c9ecf..aeb45611e6 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 4a313df0ce..75ff72c4da 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 -- cgit v1.2.3