The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Enrico,

> Would it make any difference if the software was relicensed by its author, 
> instead of Inria?

I guess so. I sent him an email explaining the situation. Let's see what 
happens.

The MIT branch created by Clément might work or might not work. We use tools 
which compares SW we use or deliver with essentially all SW on the internet, 
so the issue with the WTFPL would likely still show up in case we would in 
some future create a Coq based toolchain. The issue is not really a legal 
issue, but it would force us to put some obscenity in SW ancestry 
documentation, and this is simply a no go in an international company.

Best regards,

Michael

-----Original Message-----
From: 
coq-club-request AT inria.fr
 
[mailto:coq-club-request AT inria.fr]
 On Behalf Of Enrico Tassi
Sent: Wednesday, March 2, 2016 7:11 PM
To: 
coq-club AT inria.fr
Subject: Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts 
more readable (was Re: Lean Theorem Prover)

On Wed, Mar 02, 2016 at 05:06:33PM +0000, Soegtrop, Michael wrote:
> Of cause the WTFPL would also allow to relicense it say under LGPL 
> like Coq. So INRIA could do this and publish all under LGPL. But then 
> some corporate users will likely find out (there are automated tools 
> for this) and wonder why INRIA changes the license and maybe start 
> bothering you with questions around this.

Would it make any difference if the software was relicensed by its author, 
instead of Inria?

Best
--
Enrico Tassi
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928