Stream: Coq users

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


view this post on Zulip Paolo Giarrusso (Jul 05 2022 at 20:26):

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

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Jul 05 2022 at 20:37):

Fair enough, fixed here and on github.


Last updated: Feb 04 2023 at 21:02 UTC