From 4fd27468890065a9d529d0c58ceb6f4c19ce1f03 Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 18:51:38 -0500 Subject: Update debian/copyright --- debian/copyright | 41 +++++++++++++++++++++++++++++++++-------- 1 file changed, 33 insertions(+), 8 deletions(-) diff --git a/debian/copyright b/debian/copyright index 171d8dd0..0740aa18 100644 --- a/debian/copyright +++ b/debian/copyright @@ -7,11 +7,15 @@ Files: * 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/* +Files: config/* dev/* ide/* interp/* 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/diff2.ml +Copyright: 2016 OOHASHI Daichi +License: Expat + Files: clib/predicate.ml Copyright: 1996 Institut National de Recherche en Informatique et en Automatique License: LGPL-2+ @@ -32,17 +36,19 @@ Files: dev/tools/coqdev.el Copyright: 2018 The Coq Development Team License: LGPL-2.1 -Files: ide/utils/* +Files: ide/configwin.ml + ide/configwin.mli + ide/configwin_ihm.ml + ide/configwin_ihm.mli + ide/configwin_messages.ml + ide/configwin_types.ml 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 +Files: ide/protocol/xml_lexer.mli + ide/protocol/xml_lexer.mll + ide/protocol/xml_parser.mli Copyright: 2003 Nicolas Cannasse - 2003 Jacques Garrigue License: LGPL-2.1+ Files: plugins/micromega/sos.ml plugins/micromega/sos_lib.ml @@ -59,6 +65,25 @@ Files: test-suite/interactive/ParalITP_smallproofs.v Copyright: 1999-2017 The Coq development team, INRIA, CNRS, LIX, LRI, PPS License: LGPL-2.1+ +License: Expat + Permission is hereby granted, free of charge, to any person obtaining a copy of + this software and associated documentation files (the "Software"), to deal in + the Software without restriction, including without limitation the rights to + use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies + of the Software, and to permit persons to whom the Software is furnished to do + so, subject to the following conditions: + . + The above copyright notice and this permission notice shall be included in all + copies or substantial portions of the Software. + . + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + SOFTWARE. + 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 -- cgit v1.2.3