Le Thu, 29 Apr 2004 11:57:02 +0200 Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> a écrit : > > > I had started to work on it but stopped when I learned that coq > > > 8.0 combines GPL code with QPL code. > > I didn't know about that. I have just rgrep-ed QPL in the Coq V8.0 > source tree (CVS version) and I have found no instance of the word > QPL. What informations have you got exactly? > In the sources downldable from the website: % 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. What is also very worrying I think is: % rgrep "GNU General Public License" . -l ./contrib/jprover/jall.ml ./contrib/jprover/jtunify.ml ./contrib/xml/acic.ml ./contrib/xml/acic2Xml.ml4 ./contrib/xml/cic.dtd ./contrib/xml/cic2acic.ml ./contrib/xml/doubleTypeInference.ml ./contrib/xml/doubleTypeInference.mli ./contrib/xml/proof2aproof.ml ./contrib/xml/proofTree2Xml.ml4 ./contrib/xml/theoryobject.dtd ./contrib/xml/unshare.ml ./contrib/xml/unshare.mli ./contrib/xml/xml.ml4 ./contrib/xml/xml.mli ./contrib/xml/xmlcommand.ml ./contrib/xml/xmlcommand.mli ./contrib/xml/xmlentries.ml4 ./ide/utils/configwin.ml ./ide/utils/configwin_html_config.ml ./ide/utils/configwin_ihm.ml ./ide/utils/configwin_keys.ml ./ide/utils/configwin_messages.ml ./ide/utils/configwin_types.ml ./ide/utils/okey.ml ./tools/coq-inferior.el (the whole project seems to be under the GPL!) Cheers, Sam.
Attachment:
pgpBmL1MEqPw_.pgp
Description: PGP signature