Moving closed notations at level 0 in anticipation of the removal of the Coq fallback ignoring levels when nothing else applies. #134
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Hi, as indicated in the title, this PR is in anticipation of a change of Coq's parsing rules (see e.g. coq/coq#17876 for details). For instance, Δ( c ), formerly at level 90, was used on the right of↓, which was expecting a notation at level less than 90. As another example, ⟨πD,πC⟩, formerly at level 100, was used as argument of ◯, as if it were at level less than 40.
So, the PR moves to level 0 the notations that have terminals on both sides (in general, there is little to gain not to do so, the only problem being if the starting symbol is also ending another notation).
There is another small change, requiring extra parentheses in the argument of the prefix notations
`1
and`2
.If you agree with the change, this can be merged without delays.