aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/LICENSE
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-03-06 14:00:50 +0100
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-03-06 14:00:50 +0100
commitd095b1f2c39a9a3c0b009675573ea34034ffe52c (patch)
tree19b49f17d23b419e0579c3aa369b43ef6da2b7ac /doc/LICENSE
parent67a28c487fc64e2c0f8271b77d0c9db0cd82fa92 (diff)
Remove outdated information regarding the FAQ.
The FAQ is not part of the Coq sources anymore.
Diffstat (limited to 'doc/LICENSE')
-rw-r--r--doc/LICENSE10
1 files changed, 0 insertions, 10 deletions
diff --git a/doc/LICENSE b/doc/LICENSE
index ada22e669..0aa0d629e 100644
--- a/doc/LICENSE
+++ b/doc/LICENSE
@@ -25,16 +25,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 FAQ (Coq for the Clueless) is a work by Pierre Castéran, Hugo
-Herbelin, Florent Kirchner, Benjamin Monate, and Julien Narboux. All
-documents (the LaTeX source and the PostScript, PDF and html outputs)
-are copyright (c) INRIA 2004-2006. The material connected to the FAQ
-(Coq for the Clueless) 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 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