aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/LICENSE
diff options
context:
space:
mode:
Diffstat (limited to 'doc/LICENSE')
-rw-r--r--doc/LICENSE18
1 files changed, 10 insertions, 8 deletions
diff --git a/doc/LICENSE b/doc/LICENSE
index 7ae31b089..c223a4e16 100644
--- a/doc/LICENSE
+++ b/doc/LICENSE
@@ -2,15 +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, with the exception of the Ubuntu font files
-(UbuntuMono-Square.ttf and UbuntuMono-B.ttf), derived from UbuntuMono-Regular,
-which is Copyright 2010,2011 Canonical Ltd and licensed under the Ubuntu font
+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). 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.
+(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,