summaryrefslogtreecommitdiff
path: root/doc/LICENSE
diff options
context:
space:
mode:
Diffstat (limited to 'doc/LICENSE')
-rw-r--r--doc/LICENSE6
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/LICENSE b/doc/LICENSE
index 99087480..ada22e66 100644
--- a/doc/LICENSE
+++ b/doc/LICENSE
@@ -8,7 +8,7 @@ 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 Tutorial is a work by Gérard Huet, Gilles Kahn and Christine
+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
@@ -25,7 +25,7 @@ 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
+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
@@ -36,7 +36,7 @@ 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
+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