Format: http://www.debian.org/doc/packaging-manuals/copyright-format/1.0/
Upstream-Name: jsCoq
Upstream-Contact: Emilio J. Gallego Arias <e+jscoq@x80.org>
Source: https://github.com/ejgallego/jscoq
License: AGPL-3+
Copyright: 2015, MINES ParisTech

Authors: Emilio J. Gallego Arias
         Benoît Pin

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

Files: ui-images/checked.png
License: CC-BY 3.0
Comment:
  - Check button made by Google from www.flaticon.com, licensed under CC BY 3.0

Files: ui-images/dl.png
License: CC-BY 3.0
Comment: Cloud button made by Yannick, yanlu.de from www.flaticon.com, licensed under CC BY 3.0

Files: ui-images/power-button-512-black.png
License: CC-BY 3.0
Comment: Power buton made by Freepik, www.freepik.com from www.flaticon.com, licensed under CC BY 3.0

Files: ui-images/log-*
License: BSD
Comment: Log levels icons are from the firebug project, getfirebug.com, licensed under BSD License

Files: ui-images/*
License: AGPL-3
Comment: Other graphics are parts, and so licenced, as JsCoq.

Files: examples/Stlc.html
LICENSE: BSD
Comment: From http://https://www.cis.upenn.edu/~bcpierce/sf/

Files: ui-external/*
Comment: The frameworks in external, pace, codemirror, etc... are under their
         own licence, see the directories for more details.

# Regarding Coq and derivatives:

We currently have no "direct derivative" from Coq, which is under the
LGPL 2.1, however:

  - jscoq.ml was based on Coq's source at some point.

  - the Ocaml code in icoq.ml is tightly integrated with Coq, it could
    be considered to derive from it.