Stream: Coq users

Topic: Rejecting alphanumeric notations + identifier without a s...

Paolo Giarrusso (Jul 05 2022 at 20:26):

Posted on https://github.com/coq/coq/issues/4712#issuecomment-1175466710 which seems most related.

Gaëtan Gilbert (Jul 05 2022 at 20:30):

the Definition A should be before the Fail otherwise it doesn't test quite the right thing

Paolo Giarrusso (Jul 05 2022 at 20:37):

Fair enough, fixed here and on github.

Last updated: Feb 04 2023 at 21:02 UTC