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: Clément Pit--Claudel <clement.pit AT gmail.com>
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 10:51:32 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=clement.pit AT gmail.com; spf=SoftFail smtp.mailfrom=clement.pit AT gmail.com; spf=None smtp.helo=postmaster AT mout.kundenserver.de
Ironport-phdr: 9a23:1NPYvxRBS7rAeyOU+RkMy9MCF9psv+yvbD5Q0YIujvd0So/mwa64YBGN2/xhgRfzUJnB7Loc0qyN4/+mBjZLsMjJmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbvipNuMOU4Z2nKUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGfayQ6NtRrtBST8iLmod5cvxtBCFQxHcyGEbVzA9lptNDg7Z2yn7QtK0mS/zq+Zw3GHONsn7SL0yRXK67rtDRxrhiSNBPDk8pjKEwvdshb5W9Ury7yd0xJTZNdmY

On 03/02/2016 10:06 AM, 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.

Feel free to use this MIT licensed fork:
https://github.com/cpitclaudel/wincompose

Clément.

Attachment: signature.asc
Description: OpenPGP digital signature

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