From 6400bafe7d380bfec1fb1ae817dd3a9b275da973 Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Mon, 24 Dec 2018 21:33:52 -0500 Subject: debian/copyright: Audit and update --- debian/copyright | 128 ++++++++++++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 121 insertions(+), 7 deletions(-) diff --git a/debian/copyright b/debian/copyright index 51d61696..171d8dd0 100644 --- a/debian/copyright +++ b/debian/copyright @@ -1,20 +1,134 @@ Format: https://www.debian.org/doc/packaging-manuals/copyright-format/1.0/ -Packaged-By: Fernando Sanchez -Packaged-Date: Fri, 03 Dec 1999 22:06:04 +0100 -Source: http://coq.inria.fr/ +Upstream-Name: Coq +Source: https://github.com/coq/coq, modified to remove non-free parts +License: LGPL-2.1 Files: * -Copyright: 1999-2015 The Coq development team, INRIA, CNRS, University Paris Sud, University Paris 7, Ecole Polytechnique +Copyright: 1999-2018 The Coq Development Team, INRIA, CNRS and contributors +License: LGPL-2.1 + +Files: config/* dev/* ide/* interp/* intf/* kernel/* lib/* library/* parsing/* + pretyping/* proofs/* tactics/* test-suite/* theories/* tools/* toplevel/* +Copyright: 1999-2017 The Coq development team, INRIA, CNRS, LIX, LRI, PPS License: LGPL-2.1 +Files: clib/predicate.ml +Copyright: 1996 Institut National de Recherche en Informatique et en Automatique +License: LGPL-2+ + Files: debian/* Copyright: 1999-2000 Fernando Sanchez 2001-2002 Judicael Courant 2004-2009 Samuel Mimram 2008-2014 Stéphane Glondu + 2018 Benjamin Barenblat License: LGPL-2.1 +Files: dev/build/windows/* +Copyright: 2016 Intel Deutschland GmbH +License: LGPL-2.1+ + +Files: dev/tools/coqdev.el +Copyright: 2018 The Coq Development Team License: LGPL-2.1 - The Coq Proof Assistant is distributed under the terms of the GNU - Lesser General Public Licence, version 2.1, see - `/usr/share/common-licenses/LGPL-2.1'. + +Files: ide/utils/* +Copyright: 2005 Institut National de Recherche en Informatique et en Automatique +License: LGPL-2+ + +Files: ide/xml_lexer.mli ide/xml_lexer.mll ide/xml_parser.mli +Copyright: 2003 Nicolas Cannasse +License: LGPL-2.1+ + +Files: ide/xml_lexer.mli ide/xml_lexer.mll ide/xml_parser.ml +Copyright: 2003 Nicolas Cannasse + 2003 Jacques Garrigue +License: LGPL-2.1+ + +Files: plugins/micromega/sos.ml plugins/micromega/sos_lib.ml +Copyright: 1998 University of Cambridge + 1998-2006 John Harrison +License: HOLLight + +Files: test-suite/bugs/closed/1918.v +Copyright: Ralph Matthes, I.R.I.T., C.N.R.S. & University of Toulouse +License: LGPL-2.1 + +Files: test-suite/interactive/ParalITP_smallproofs.v + test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v +Copyright: 1999-2017 The Coq development team, INRIA, CNRS, LIX, LRI, PPS +License: LGPL-2.1+ + +License: HOLLight + HOL Light version 2.20, hereinafter referred to as "the software", is a + computer theorem proving system written by John Harrison. Much of the software + was developed at the University of Cambridge Computer Laboratory, New Museums + Site, Pembroke Street, Cambridge, CB2 3QG, England. The software is copyright, + University of Cambridge 1998 and John Harrison 1998-2006. + . + Permission to use, copy, modify, and distribute the software and its + documentation for any purpose and without fee is hereby granted. In the case of + further distribution of the software the present text, including copyright + notice, licence and disclaimer of warranty, must be included in full and + unmodified form in any release. Distribution of derivative software obtained by + modifying the software, or incorporating it into other software, is permitted, + provided the inclusion of the software is acknowledged and that any changes + made to the software are clearly documented. + . + John Harrison and the University of Cambridge disclaim all warranties with + regard to the software, including all implied warranties of merchantability and + fitness. In no event shall John Harrison or the University of Cambridge be + liable for any special, indirect, incidental or consequential damages or any + damages whatsoever, including, but not limited to, those arising from computer + failure or malfunction, work stoppage, loss of profit or loss of contracts. + +License: LGPL-2+ + This library is free software; you can redistribute it and/or modify it under + the terms of the GNU Library General Public License as published by the Free + Software Foundation; either version 2 of the License, or (at your option) any + later version. + . + This library is distributed in the hope that it will be useful, but WITHOUT ANY + WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A + PARTICULAR PURPOSE. See the GNU Library General Public License for more + details. + . + You should have received a copy of the GNU Library General Public License along + with this library; if not, write to the Free Software Foundation, Inc., 51 + Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA + . + On Debian systems, the complete text of the GNU Library General Public License + version 2 can be found in "/usr/share/common-licenses/LGPL-2". + +License: LGPL-2.1 + This library is free software; you can redistribute it and/or modify it under + the terms of the GNU Lesser General Public License, version 2.1, as published + by the Free Software Foundation. + . + This library is distributed in the hope that it will be useful, but WITHOUT ANY + WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A + PARTICULAR PURPOSE. See the GNU Lesser General Public License for more details. + . + You should have received a copy of the GNU Lesser General Public License along + with this library; if not, write to the Free Software Foundation, Inc., 51 + Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA + . + On Debian systems, the complete text of the GNU Lesser General Public License + version 2.1 can be found in "/usr/share/common-licenses/LGPL-2.1". + +License: LGPL-2.1+ + This library is free software; you can redistribute it and/or modify it under + the terms of the GNU Lesser General Public License as published by the Free + Software Foundation; either version 2.1 of the License, or (at your option) any + later version. + . + This library is distributed in the hope that it will be useful, but WITHOUT ANY + WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A + PARTICULAR PURPOSE. See the GNU Lesser General Public License for more details. + . + You should have received a copy of the GNU Lesser General Public License along + with this library; if not, write to the Free Software Foundation, Inc., 51 + Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA + . + On Debian systems, the complete text of the GNU Lesser General Public License + version 2.1 can be found in "/usr/share/common-licenses/LGPL-2.1". -- cgit v1.2.3