Copyright for coq-doc source package in Focal

Format: https://www.debian.org/doc/packaging-manuals/copyright-format/1.0/
Packaged-By: Fernando Sanchez 
Packaged-Date: Sun, 28 Nov 1999 19:42:06 +0100
Upstream-Author: The Coq Development Team
Source: http://coq.inria.fr/
Comment:
 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
Comment:
 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: OPL-1.0
Comment:
 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: OPL-1.0
Comment:
 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: LGPL-2.1
Comment:
 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: OPL-1.0
Comment:
 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: OPL-1.0
Comment:
 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 
           2002, Judicaël Courant 
           2004-2010, Samuel Mimram 
           2010-2014, Stéphane Glondu 
License: LGPL-2.1

License: LGPL-2.1
 This software 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.

License: OPL-1.0
 .
                       *Open Publication License*
                            v1.0, 8 June 1999
 .
 .
 *I. REQUIREMENTS ON BOTH UNMODIFIED AND MODIFIED VERSIONS*
 .
 The Open Publication works may be reproduced and distributed in whole or
 in part, in any medium physical or electronic, provided that the terms
 of this license are adhered to, and that this license or an
 incorporation of it by reference (with any options elected by the
 author(s) and/or publisher) is displayed in the reproduction.
 .
 Proper form for an incorporation by reference is as follows:
 .
     Copyright (c)  by . This material
     may be distributed only subject to the terms and conditions set
     forth in the Open Publication License, vX.Y or later (the latest
     version is presently available at http://www.opencontent.org/openpub/).
 .
 The reference must be immediately followed with any options elected by
 the author(s) and/or publisher of the document (see section VI).
 .
 Commercial redistribution of Open Publication-licensed material is
 permitted.
 .
 Any publication in standard (paper) book form shall require the citation
 of the original publisher and author. The publisher and author's names
 shall appear on all outer surfaces of the book. On all outer surfaces of
 the book the original publisher's name shall be as large as the title of
 the work and cited as possessive with respect to the title.
 .
 .
 *II. COPYRIGHT*
 .
 The copyright to each Open Publication is owned by its author(s) or
 designee.
 .
 .
 *III. SCOPE OF LICENSE*
 .
 The following license terms apply to all Open Publication works, unless
 otherwise explicitly stated in the document.
 .
 Mere aggregation of Open Publication works or a portion of an Open
 Publication work with other works or programs on the same media shall
 not cause this license to apply to those other works. The aggregate work
 shall contain a notice specifying the inclusion of the Open Publication
 material and appropriate copyright notice.
 .
 SEVERABILITY. If any part of this license is found to be unenforceable
 in any jurisdiction, the remaining portions of the license remain in force.
 .
 NO WARRANTY. Open Publication works are licensed and provided "as is"
 without warranty of any kind, express or implied, including, but not
 limited to, the implied warranties of merchantability and fitness for a
 particular purpose or a warranty of non-infringement.
 .
 .
 *IV. REQUIREMENTS ON MODIFIED WORKS*
 .
 All modified versions of documents covered by this license, including
 translations, anthologies, compilations and partial documents, must meet
 the following requirements:
 .
    1. The modified version must be labeled as such.
    2. The person making the modifications must be identified and the
       modifications dated.
    3. Acknowledgement of the original author and publisher if applicable
       must be retained according to normal academic citation practices.
    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.
 .
 .
 *V. GOOD-PRACTICE RECOMMENDATIONS *
 .
 In addition to the requirements of this license, it is requested from
 and strongly recommended of redistributors that:
 .
    1. If you are distributing Open Publication works on hardcopy or
       CD-ROM, you provide email notification to the authors of your
       intent to redistribute at least thirty days before your manuscript
       or media freeze, to give the authors time to provide updated
       documents. This notification should describe modifications, if
       any, made to the document.
    2. All substantive modifications (including deletions) be either
       clearly marked up in the document or else described in an
       attachment to the document.
    3. Finally, while it is not mandatory under this license, it is
       considered good form to offer a free copy of any hardcopy and
       CD-ROM expression of an Open Publication-licensed work to its
       author(s).
 .
 .
 *VI. LICENSE OPTIONS*
 .
 The author(s) and/or publisher of an Open Publication-licensed document
 may elect certain options by appending language to the reference to or
 copy of the license. These options are considered part of the license
 instance and must be included with the license (or its incorporation by
 reference) in derived works.
 .
 A. To prohibit distribution of substantively modified versions without
 the explicit permission of the author(s). "Substantive modification" is
 defined as a change to the semantic content of the document, and
 excludes mere changes in format or typographical corrections.
 .
 To accomplish this, add the phrase `Distribution of substantively
 modified versions of this document is prohibited without the explicit
 permission of the copyright holder.' to the license reference or copy.
 .
 B. To prohibit any publication of this work or derivative works in whole
 or in part in standard (paper) book form for commercial purposes is
 prohibited unless prior permission is obtained from the copyright holder.
 .
 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.