coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover)

From: Enrico Tassi <enrico.tassi AT inria.fr>
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)
Date: Wed, 2 Mar 2016 19:10:46 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=enrico.tassi AT inria.fr; spf=None smtp.mailfrom=gares AT fettunta.org; spf=None smtp.helo=postmaster AT fettunta.org
Ironport-phdr: 9a23:RvG7gBYP4DHOrZY2WLvreRj/LSx+4OfEezUN459isYplN5qZpc+9bnLW6fgltlLVR4KTs6sC0LqJ9f+6Ej1eqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLsh7/0pMeYMlsArQH+SI0xBS3+lR/WuMgSjNkqAYcK4TyNnEF1ff9Lz3hjP1OZkkW0zM6x+Jl+73YY4Kp5pIYTGZn9Kq8/VPlTCCksG2Ez/szi8xfZHiWV4X5Jf2MMkxFPSzTM9wr7FsP8tDH7ve07xCCBJszeTLYuWD3k4b09G0ygszsOKzNsqDKfscd3lq8O+B8=

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

Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), (continued)