aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/sphinx
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-06-24 10:23:43 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-06-24 10:23:43 +0200
commitdbd83db207588fa3a87d44dbf01dee318f4db9c9 (patch)
treec6376866d67a3de157dc09a99ee5004f0823c58c /doc/sphinx
parentac543a0fe77ea794cc8324e102701ee1eddc7c01 (diff)
parentb33aa9bd9760b8de73709f9e11f63b1ae9da07b1 (diff)
Merge PR #7784: Remove Tutorials from a few other places following #7466.
Diffstat (limited to 'doc/sphinx')
-rw-r--r--doc/sphinx/introduction.rst7
1 files changed, 0 insertions, 7 deletions
diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst
index 20e4069f4..bc72877b6 100644
--- a/doc/sphinx/introduction.rst
+++ b/doc/sphinx/introduction.rst
@@ -103,13 +103,6 @@ List of additional documentation
This manual does not contain all the documentation the user may need
about |Coq|. Various informations can be found in the following documents:
-Tutorial
- A companion volume to this reference manual, the |Coq| Tutorial, is
- aimed at gently introducing new users to developing proofs in |Coq|
- without assuming prior knowledge of type theory. In a second step,
- the user can read also the tutorial on recursive types (document
- `RecTutorial.ps`).
-
Installation
A text file `INSTALL` that comes with the sources explains how to
install |Coq|.