diff --git a/CHANGES.md b/CHANGES.md index add23705..c9769f4c 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,6 +1,8 @@ ## unreleased - - [general] Cleanup old / unused code (@ejgallego, #) + - [general] Cleanup old / unused code (@ejgallego, #362) + - [general] Make licensing clearer (@ejgallego @palmskog + @SnarkBoojum, #361, closes #266) ## Version 0.18.1: diff --git a/LICENSE b/LICENSE index 8b88e2c9..5670fcff 100644 --- a/LICENSE +++ b/LICENSE @@ -3,22 +3,20 @@ Upstream-Name: coq-serapi Upstream-Contact: Emilio J. Gallego Arias Source: https://github.com/ejgallego/coq-serapi License: LGPL-2.1+ -Copyright: 2016-2022, MINES ParisTech / Inria +Copyright: 2016-2023, MINES ParisTech / Inria / others +Authors: Emilio J. Gallego Arias, Karl Palmskog, Clément Pit-Claudel, Kaiyu Yang -Authors: Emilio J. Gallego Arias +Files: serlib/* serapi/* sertop/* +License: LGPL-2.1+ +Copyright: 2016-2023, MINES ParisTech / Inria / others Files: notes/* License: LGPL-2.1+ / CC-BY-SA 3.0 -Files: jscoq/* -License: GPL-3+ - Files: tests/genarg/* Authors: Karl Palmskog Licence: Derived from many projects as test cases, falls into fair-use Comment: the intent is to be compatible with Coq's license. Note that -the LGPL-2.1+ allows to treat the code as GPL-3+ , and we favor -that. In some cases, like when linking with jsCoq's code or other code -that is GPL-3 only, the resulting .js or binaries files will be GPL-3. +the LGPL-2.1+ allows to treat the code as GPL-3+ , and we favor that. diff --git a/coq-serapi.opam b/coq-serapi.opam index 880df1f1..a3434187 100644 --- a/coq-serapi.opam +++ b/coq-serapi.opam @@ -3,7 +3,7 @@ maintainer: "e@x80.org" homepage: "https://github.com/ejgallego/coq-serapi" bug-reports: "https://github.com/ejgallego/coq-serapi/issues" dev-repo: "git+https://github.com/ejgallego/coq-serapi.git" -license: "GPL-3.0-or-later" +license: "LGPL-2.1-or-later" doc: "https://ejgallego.github.io/coq-serapi/" synopsis: "Serialization library and protocol for machine interaction with the Coq proof assistant"