aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-04-05 11:58:43 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-04-05 11:58:43 +0000
commit2ac5b6fd1ee5465c82a7f3107befc6fed22e2228 (patch)
treebb9acbcf58f37adcb969b6f9eb697f672e205ff4
parent004484f8406428df8c9ce0852d1c083a9125c3dc (diff)
MAJ Licence FAQ
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8682 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--doc/LICENCE21
1 files changed, 13 insertions, 8 deletions
diff --git a/doc/LICENCE b/doc/LICENCE
index caf71129d..12b51664a 100644
--- a/doc/LICENCE
+++ b/doc/LICENCE
@@ -6,7 +6,7 @@ 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/).
-Note that options A and B are *not* elected.
+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,
@@ -19,12 +19,17 @@ package. All related documents (the Coq vernacular source files and
the PostScript, PDF and html outputs) are copyright (c) INRIA
1999-2006. The material connected to the Standard Library is
distributed under the terms of the Lesser General Public License
-version 2.1 or later.
-
-The FAQ 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 and come with no 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
@@ -33,7 +38,7 @@ BibTeX sources and the PostScript, PDF and html outputs) are copyright
[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/). Note that options A and B are
+http://www.opencontent.org/openpub/). Options A and B are
*not* elected.
----------------------------------------------------------------------