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: [EMAIL PROTECTED] http://www.cs.unibo.it/~sacerdot ---------------------------------------------------------------- -- To UNSUBSCRIBE, email to [EMAIL PROTECTED] with a subject of "unsubscribe". Trouble? Contact [EMAIL PROTECTED]