Bas Spitters
Bas Spitters
Recording an email discussion with @mattam82 the main issue is binding of the constants used by Equations, and probably a bit of fidling with the current Coq proofs the theories/...
I meant: you are also introducing a new class of propositions. Do the stdlib and all the tactics continue to work out of the box? If not, how do you...
I think it's a good start. Not sure what to do about congruence. @mattam82 ?
Since you are working on Equations. It may help to include @cmangin .
I agree with your recommendation! On Wed, Aug 10, 2022 at 3:48 PM Théo Zimmermann ***@***.***> wrote: > @spitters @VincentSe > : do you prefer to release e34e331 > >...
Thanks! On Sat, Aug 20, 2022 at 2:16 PM Théo Zimmermann ***@***.***> wrote: > I've pushed a new 8.16.0 tag and a PR coq/opam-coq-archive#2261 > . > > — >...
That would be great. Please send a PR.
Multi licensing could be a possibility, but there doesn't seem to be a reason to go for LGPL, over MIT/BSD. So, I agree with @Zimmi48 and @robbertkrebbers that the latter...
Corn has had MIT code in the fast/ directory since 2007.
@herbelin your description of the history is correct. In fact, I'm aware of only one strong GPL proponent, who has since long left academia.