Yannick Forster

icon indicating a website link https://yforster.de icon indicating an email [email protected]

icon company Inria icon location Paris icon location Researcher in the Cambium Team at Inria Paris

Results 43 comments of Yannick Forster

Consider changing to a permissive or weak copyleft license

My understanding is that MIT and MPL are relatively similar, but the difference is that if somebody changes our code, they have to publish this code under MPL license again....

`Scheme Case` and `Scheme Elimination` do not match `Set Case Analysis Schemes`

I think this is a bug of `Scheme Case` and `Scheme Elimination`. They should be the non-recursive equivalents for `Scheme Minimality` and `Scheme Induction`, but unfortunately they are the respective...

`Scheme Case` and `Scheme Elimination` do not match `Set Case Analysis Schemes`

I think the reason is that lines 331 and 332 in [indschemes.ml](https://github.com/coq/coq/blob/7153cc3a4d886944f9e09a10ea106cefb1e9d0f8/vernac/indschemes.ml#L331) are exactly the same, so `CaseScheme` and `IndScheme` are never distinguished in the code and the `Scheme` command...