Re: COQ 8.0

[Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>]

 I can give some more explications.

> % rgrep "Q Public" . -l
> ./ide/utils/configwin.mli
> ./ide/utils/okey.mli

> Those files seem to come from Cameleon which is now licensed under the
> GPL.

 Right. These are QPLed. Thes two files are necessary only to
 coqide. Of course coqide is interesting, but it should be a separate
 package from the rest of Coq (since it depends on lablgtk).
 Thus this does not inhibit packaging the core Coq.

> What is also very worrying I think is:

> ./contrib/xml/*

 Right: the COPYRIGHT file states that the licensee is the same as  Coq,
 but I put the GPL header in the files (I am the main author of
 contrib/xml). I am willing to change it if requested to.

> ./ide/*

 As before, this is a separate component (mix of QPL, LGPL, GPL).
 I do not know whether this affects or  not the rest of Coq.

> ./contrib/jprover/jtunify.ml

 Originaly part of MetaPRL. It could be debranched since no contrib
 uses it yet (to my knowledge). It would be a pity, though.

> ./tools/coq-inferior.el

 I do not know much about this. It provides emacs modes for Coq.
 The author is probably willing to change the licence, but the file
 is a modification of an older file that could be GPLed.

					Hope it helps,
					   C.S.C.

-- 
----------------------------------------------------------------
Real name: Claudio Sacerdoti Coen
PhD Student in Computer Science at University of Bologna
E-mail: sacerdot@cs.unibo.it
http://www.cs.unibo.it/~sacerdot
----------------------------------------------------------------