Merge PR #7784: Remove Tutorials from a few other places following #7466.

2 files changed, 0 insertions, 26 deletions

diff --git a/doc/LICENSE b/doc/LICENSE
index c223a4e16..c9f574afb 100644
--- a/doc/LICENSE
+++ b/doc/LICENSE
@@ -14,15 +14,6 @@ License, v1.0 or later (the latest version is presently available at
 http://www.opencontent.org/openpub/).  Options A and B are *not*
 elected.
 
-The Coq Tutorial is a work by Gérard Huet, Gilles Kahn and Christine
-Paulin-Mohring. All documents (the LaTeX source and the PostScript,
-PDF and html outputs) are copyright (c) INRIA 1999-2006. The material
-connected to the Coq Tutorial may be distributed only subject to the
-terms and conditions set forth in the Open Publication License, v1.0
-or later (the latest version is presently available at
-http://www.opencontent.org/openpub/). Options A and B are *not*
-elected.
-
 The Coq Standard Library is a collective work from the Coq Development
 Team whose members are listed in the file CREDITS of the Coq source
 package. All related documents (the Coq vernacular source files and
@@ -31,16 +22,6 @@ the PostScript, PDF and html outputs) are copyright (c) INRIA
 distributed under the terms of the Lesser General Public License
 version 2.1 or later. 
 
-The Tutorial on [Co-]Inductive Types in Coq is a work by Pierre
-Castéran and Eduardo Gimenez. All related documents (the LaTeX and
-BibTeX sources and the PostScript, PDF and html outputs) are copyright
-(c) INRIA 1997-2006. The material connected to the Tutorial on
-[Co-]Inductive Types in Coq may be distributed only subject to the
-terms and conditions set forth in the Open Publication License, v1.0
-or later (the latest version is presently available at
-http://www.opencontent.org/openpub/).  Options A and B are
-*not* elected.
-
 ----------------------------------------------------------------------
 
                       *Open Publication License*
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|.