diff options
Diffstat (limited to 'doc/sphinx/introduction.rst')
| -rw-r--r-- | doc/sphinx/introduction.rst | 15 |
1 files changed, 7 insertions, 8 deletions
diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst index 514745c1b..75ff72c4d 100644 --- a/doc/sphinx/introduction.rst +++ b/doc/sphinx/introduction.rst @@ -2,12 +2,11 @@ Introduction ------------------------ -This document is the Reference Manual of version 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 @@ -60,7 +59,7 @@ continuous reading. However, it has some structure that is explained below. - The first part describes the specification language, |Gallina|. - Chapters :ref:`thegallinaspecificationlanguage` and :ref:`extensionsofgallina` describe the concrete + Chapters :ref:`gallinaspecificationlanguage` and :ref:`extensionsofgallina` describe the concrete syntax as well as the meaning of programs, theorems and proofs in the Calculus of Inductive Constructions. Chapter :ref:`thecoqlibrary` describes the standard library of |Coq|. Chapter :ref:`calculusofinductiveconstructions` is a mathematical description @@ -76,7 +75,7 @@ below. Chapter :ref:`proofhandling`. In Chapter :ref:`tactics`, all commands that realize one or more steps of the proof are presented: we call them *tactics*. The language to combine these tactics into complex proof - strategies is given in Chapter :ref:`thetacticlanguage`. Examples of tactics + strategies is given in Chapter :ref:`ltac`. Examples of tactics are described in Chapter :ref:`detailedexamplesoftactics`. - The third part describes how to extend the syntax of |Coq|. It |