[Pkg-ocaml-maint-commits] [SCM] coq-doc packaging branch, master, updated. debian/8.1-3-27-gabb5c8e

Thu Jan 7 21:53:37 UTC 2010

The following commit has been merged in the master branch:
commit 5ea6a0607685202a2025a4956aef07428ac94344
Author: Stephane Glondu <steph at glondu.net>
Date:   Thu Jan 7 22:25:53 2010 +0100

    New copyright file

diff --git a/debian/copyright b/debian/copyright
index ae548ef..af0fba1 100644
--- a/debian/copyright
+++ b/debian/copyright
@@ -1,54 +1,110 @@
-This package was debianized by Fernando Sanchez <fer at debian.org> on
-Sun, 28 Nov 1999 19:42:06 +0100.
-
-
-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.
-
-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
-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 Standard Library 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 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.
-See /usr/share/common-licenses/LGPL.
-
-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
-(c) INRIA 1997-2006. The material connected to the Tutorial on
-[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/).  Options A and B are
-*not* elected.
+Packaged-By: Fernando Sanchez <fer at debian.org>
+Packaged-Date: Sun, 28 Nov 1999 19:42:06 +0100
+Upstream-Author: The Coq Development Team
+Original-Source-Location: http://coq.inria.fr/
+
+
+  Note: The Coq proof assistant itself is DFSG-free and packaged in
+  Debian (main). However, its documentation is under OPL, a license
+  which is not considered DFSG-free. See:
+
+    http://lists.debian.org/debian-legal/2004/03/msg00226.html
+
+
+Files: *
+Copyright: © 1999-2004 The Coq development team,
+                       INRIA-CNRS, University Paris Sud
+License: LGPL-2.1
+
+  The Coq proof assistant is distributed under the terms of the GNU
+  Lesser General Public License, version 2.1. On Debian systems, the
+  full text can be found in /usr/share/common-licenses/LGPL-2.1.
+
+  The Coq proof assistant V7 and V8 includes software developed by the
+  Coq development team inside the TypiCal (formerly LogiCal) project,
+  at INRIA, CNRS and University Paris Sud.
+
+  Copyright 1999-2004 The Coq development team, INRIA-CNRS, University
+  Paris Sud, All rights reserved.
+
+  This product includes also software developed by many external
+  contributors, see /usr/share/coq-doc/CREDITS.gz and the credits
+  section in the introduction of the Reference Manual.
+
+Files: doc/refman/*
+Copyright: © 1999-2006 INRIA
+License: other
+
+  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.
+
+Files: doc/tutorial/*
+Copyright: © 1999-2006 INRIA
+License: other
+
+  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 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.
+
+Files: doc/stdlib/*
+Copyright: © 1999-2006 INRIA
+License: other
+
+  The Coq Standard Library 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 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.
+
+Files: doc/faq/*
+Copyright: © 2004-2006 INRIA
+License: other
+
+  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.
+
+Files: doc/RecTutorial/*
+Copyright: © 1997-2006 INRIA
+License: other
+
+  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 (c) INRIA 1997-2006. The material connected to the
+  Tutorial on [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/).  Options A and B
+  are *not* elected.
+
+Files: debian/*
+Copyright: © 1999 Fernando Sanchez <fer at debian.org>
+           © 2002 Judicaël Courant <Judicael.Courant at lri.fr>
+           © 2004-2010 Samuel Mimram <smimram at debian.org>
+           © 2010 Stéphane Glondu <glondu at debian.org>
+License: LGPL-2.1
 
 ----------------------------------------------------------------------
 
@@ -124,7 +180,7 @@ the following requirements:
    4. The location of the original unmodified document must be identified.
    5. The original author's (or authors') name(s) may not be used to
       assert or imply endorsement of the resulting document without the
-      original author's (or authors') permission. 
+      original author's (or authors') permission.
 
 
 *V. GOOD-PRACTICE RECOMMENDATIONS *
@@ -172,3 +228,5 @@ To accomplish this, add the phrase 'Distribution of the work or
 derivative of the work in any standard (paper) book form is prohibited
 unless prior permission is obtained from the copyright holder.' to the
 license reference or copy.
+
+----------------------------------------------------------------------

-- 
coq-doc packaging

