-
Notifications
You must be signed in to change notification settings - Fork 632
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Fixes #17583: regression using numerals in the syntax of tactic notations #17589
Fixes #17583: regression using numerals in the syntax of tactic notations #17589
Conversation
As a superficial comment, this looks very hackish to me, even for Ltac1. |
You mean that the criterion for deciding when a keyword is needed is hackish? In some sense, yes, it is hackish counterpart of not having a more local treatment of keywords. Regarding the code, otherwise, I would say that it should be factorized in one central place (except that GADT and different Term/NonTerm types make it difficult to factorize). |
2e79185
to
b0091de
Compare
b0091de
to
cc04085
Compare
After an ident, it does not need (see Metasyntax.make_production for the similar computation in constr): after another terminal, it does not need.
cc04085
to
1f13c98
Compare
What are we doing with this? |
I answered @ppedrot's remark I think. Now, the PR seen as fixing a regression passed over 3 versions probably, so maybe not any more so important either. |
Let's close thus. |
Fixes / closes #17583.
We are a bit less eager to define every terminal of a
Tactic Notation
as a keyword, following what we already did forNotation
.We make a patch also for
Ltac2 Notation
which had the same limitation (Ltac2 developers: tell if this is ok).