search

mit-plv / riscv-coq

RISC-V Specification in Coq
BSD 3-Clause "New" or "Revised" License
109 stars 17 forks source link

Adapt to Coq PR #13664: keywords starting with a number can now be effectively used in the parser #28

Closed herbelin closed 3 years ago

herbelin commented 3 years ago

With coq/coq#13664, a few riscv notations mentioning keywords starting with a number, such as 0), 24), etc., were beforehand available only for printing because the parser of numbers was hiding the keyword. The keywords are now available for parsing but now the keywords 0), 24), etc. break the parsing of common expressions such as (f 0), or even (at level 0).

We move the notations that declared these keywords explicitly to only printing, so as not to break the parsing of such common expressions.

Note: if really wanted for parsing, the notations should be at level 0 and the ) separated from the 0 or 24, etc.

If ok with the change, the PR is backward compatible (since it could not be used for parsing beforehand). It can be merged now.

samuelgruetter commented 3 years ago

Thanks! I also bumped riscv-coq in bedrock2, so it should appear on bedrock2's tested branch tomorrow.

herbelin commented 3 years ago

Thanks!