Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[license] Clarify and fix a few typos. #278

Merged
merged 2 commits into from
Sep 8, 2022
+11 −15
Merged

[license] Clarify and fix a few typos. #278

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
bbff00c
[license] Clarify and fix a few typos.
ejgallego Sep 8, 2022
9bd9a46
[jscoq] Compat with yojson >= 2.0
ejgallego Sep 8, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
22 changes: 9 additions & 13 deletions LICENSE
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,26 +2,22 @@ Format: http://www.debian.org/doc/packaging-manuals/copyright-format/1.0/
Upstream-Name: coq-serapi
Upstream-Contact: Emilio J. Gallego Arias <e@x80.org>
Source: https://github.com/ejgallego/coq-serapi
License: LGPL-2.1+ / GPL-3+
Copyright: 2016, MINES ParisTech
License: LGPL-2.1+
Copyright: 2016-2022, MINES ParisTech / Inria

Authors: Emilio J. Gallego Arias

Files: doc/*
License: GPL-3+ / CC-BY-SA 3.0 / LGPL-2.1+
Files: notes/*
License: LGPL-2.1+ / CC-BY-SA 3.0

Files: sertop/*
License: GPL-3+ / AGPL-3+
Files: jscoq/*
License: GPL-3+

Files: tests/genarg/*
Authors: Karl Palmskog
Licence: Derived from many projects as test cases, likely fall into fair-use

Comment: the intent is to be compatible with Coq, however we favor
GPL-3.

We currently have very little direct derivative from Coq, however
using LGPL 2.1 seems the safest for now, but we may move to GPL-3 at
some point, and definitively we double license everything under the
GPL3 or at your option, any later version.
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,
like when linking with jsCoq's code, the resulting .js file will be GPL-3+.

2 changes: 1 addition & 1 deletion jscoq/coq-js/jslib.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ type digest = Digest.t
type _digest = string
[@@deriving yojson]

type json = Yojson.Safe.json [@ocaml.warning "-3"]
type json = Yojson.Safe.t

let digest_of_yojson j =
let open Result in
Expand Down
2 changes: 1 addition & 1 deletion jscoq/coq-js/jslib.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ val no_files : coq_pkg -> int

(* JSON handling *)
(* XXX Use PPX *)
type json = Yojson.Safe.json [@ocaml.warning "-3"]
type json = Yojson.Safe.t

val coq_pkg_to_yojson : coq_pkg -> json
val coq_pkg_of_yojson : json -> (coq_pkg, string) Result.result
Expand Down