diff --git a/LICENSE b/LICENSE index 54458aa3..b4080fa9 100644 --- a/LICENSE +++ b/LICENSE @@ -21,6 +21,14 @@ Files: tests/genarg/* Authors: Karl Palmskog Licence: Derived from many projects as test cases, falls into fair-use +Files: tests/genarg/LibTactics.v +Authors: Arthur Chargueraud +Licence: LGPL-v3 + +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. +the LGPL-2.1+ allows to treat the code as GPL-3+ , we explicitly ack that here. diff --git a/sertop/js_sexp_printer.ml b/sertop/js_sexp_printer.ml index f4fbfed6..bb52981d 100644 --- a/sertop/js_sexp_printer.ml +++ b/sertop/js_sexp_printer.ml @@ -1,20 +1,29 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) +(** Emilio J. Gallego Arias: Code below is adapted from Jane Street's + sexplib, licence is: -(************************************************************************) -(* SerAPI: Coq interaction protocol with bidirectional serialization *) -(************************************************************************) -(* Copyright 2016-2019 MINES ParisTech -- License LGPL 2.1+ *) -(* Copyright 2019-2023 Inria -- License LGPL 2.1+ *) -(* Written by: Emilio J. Gallego Arias and others *) -(************************************************************************) +The MIT License + +Copyright (c) 2005--2024 Jane Street Group, LLC opensource-contacts@janestreet.com + +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. +*) open Format open Sexplib diff --git a/sertop/js_sexp_printer.mli b/sertop/js_sexp_printer.mli index 8e8cc0f6..63f4973b 100644 --- a/sertop/js_sexp_printer.mli +++ b/sertop/js_sexp_printer.mli @@ -1,19 +1,28 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) +(** Emilio J. Gallego Arias: Code below is adapted from Jane Street's + sexplib, licence is: -(************************************************************************) -(* SerAPI: Coq interaction protocol with bidirectional serialization *) -(************************************************************************) -(* Copyright 2016-2019 MINES ParisTech -- License LGPL 2.1+ *) -(* Copyright 2019-2023 Inria -- License LGPL 2.1+ *) -(* Written by: Emilio J. Gallego Arias and others *) -(************************************************************************) +The MIT License + +Copyright (c) 2005--2024 Jane Street Group, LLC opensource-contacts@janestreet.com + +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. +*) val pp_sertop : Format.formatter -> Sexplib.Sexp.t -> unit