aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/LICENSE
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-06-12 11:25:32 +0200
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-06-17 13:33:19 +0200
commit5734c4527befeb61249979ecf7c043a3b463fc98 (patch)
tree5cf34f455ce7658cffab88ea2d4f51e90b2c26d9 /doc/LICENSE
parent8854588be4e2e8249f6ad9d16a0fd0534d42b66d (diff)
Remove Tutorials from doc/LICENSE following #7466.
Diffstat (limited to 'doc/LICENSE')
-rw-r--r--doc/LICENSE19
1 files changed, 0 insertions, 19 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*