Re: ITP: ssreflect -- small scale reflection extension for the Coq proof assistant

2009-08-26 Thread Stéphane Glondu
MJ Ray a écrit : > I think we've consensus on software that uses CeCILL (upgradeable to > GPL, so meets DFSG) and we've discussed CeCILL-C, but what do we think > of B? My searches didn't find much discussion of it here, or any > packages in the archive using it yet. A copy follows. Please cc th

Re: GCC 4.4 run-time license and non-GPLv3 compilers

2009-04-10 Thread Stéphane Glondu
Florian Weimer a écrit : > Starting with version 4.4, the FSF the licenses the GCC run-time > library with a special exception: [...] A few precisions: * OCaml doesn't depend on any GCC-specific feature. It works with any C compiler. * There are 4 compilers for Objective Caml: - ocamlc,

Re: ITP: ssreflect -- small scale reflection extension for the Coq proof assistant

2008-12-12 Thread Stéphane Glondu
MJ Ray a écrit : > RFC from debian-legal regarding the license:- I would add that ssreflect is a plugin that is meant to be linked (dynamically) to Coq (Coq being the main program), which is LGPL-2.1. I haven't yet studied in much details any license-related incompatibilites that might occur, but