summaryrefslogtreecommitdiff
path: root/doc/LICENSE
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@debian.org>2018-12-29 14:31:27 -0500
committerGravatar Benjamin Barenblat <bbaren@debian.org>2018-12-29 14:31:27 -0500
commit9043add656177eeac1491a73d2f3ab92bec0013c (patch)
tree2b0092c84bfbf718eca10c81f60b2640dc8cab05 /doc/LICENSE
parenta4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (diff)
Imported Upstream version 8.8.2upstream/8.8.2
Diffstat (limited to 'doc/LICENSE')
-rw-r--r--doc/LICENSE26
1 files changed, 11 insertions, 15 deletions
diff --git a/doc/LICENSE b/doc/LICENSE
index ada22e66..c223a4e1 100644
--- a/doc/LICENSE
+++ b/doc/LICENSE
@@ -2,11 +2,17 @@ The Coq Reference Manual 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 LaTeX and BibTeX sources, the
embedded png files, and the PostScript, PDF and html outputs) are
-copyright (c) INRIA 1999-2006. The material connected to the Reference
-Manual 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.
+copyright (c) INRIA 1999-2006, with the exception of the Ubuntu font
+file UbuntuMono-B.ttf, which is
+Copyright 2010,2011 Canonical Ltd and licensed under the Ubuntu font
+license, version 1.0
+(https://www.ubuntu.com/legal/terms-and-policies/font-licence), and its
+derivative CoqNotations.ttf distributed under the same license. The
+material connected to the Reference Manual 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 Tutorial is a work by Gérard Huet, Gilles Kahn and Christine
Paulin-Mohring. All documents (the LaTeX source and the PostScript,
@@ -25,16 +31,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