Syntax error: [natural] expected after 'Extern' (in [hint]).

[jlottes]

Description of the problem

Tactic Notation "foo" "2" := idtac.
Global Hint Extern 2 (True) => exact I : core.

The hint command results in the error

Syntax error: [natural] expected after 'Extern' (in [hint]).

Apparently the use of "2" in quotes in the tactic notation definition makes the parser subsequently fail to recognize 2 as a natural in the hint command. The above code worked in earlier versions of Coq (maybe 8.10?). I would think either the use of "2" in Tactic Notation should be allowed and the Hint command should continue to work, or else this use of a numeral in Tactic Notation should be banned with an error message. The current error message after the Hint command is unhelpful.

Coq Version

8.17.0

[SkySkimmer]

Error appears between 8.14 and 8.15.
69d0f05 is the first bad commit (#13664)
cc @herbelin

[herbelin]

Fixing the example in the header is easy because 2 does not occur in position of needing to be declared as a keyword.

However, a more involved example where 2 would have a pivotal parsing role and thus would need to be a keyword, as in:

Tactic Notation "foo'" lconstr(x) "2" := idtac x.
Global Hint Extern 2 (True) => exact I : core.

would be less easy to fix.

Indeed, when defining Tactic Notation "foo'" lconstr(x) "2" := idtac x., it is legitimate that 2 becomes a keyword since, otherwise, foo S 2 would be interpreted as foo' (S 2) and fails to parse (which was the case before 69d0f05).

The problem is that when 2 is correctly declared as a keyword, and since keywords are global, this impacts other commands mentioning 2, such as the Hint Extern 2 above.

Ideally, keywords should be local to the rules under consideration, but that's some work (maybe not so difficult, but still some work).

Or, it could also be checked that the position of 2 in Hint Extern 2 does not critically require it to be a keyword, so it be turned back into a regular number.

Anyway, the specific example reported in the header is fixed in #17589 as well as for Ltac2 (though to fix the foo' example, it would require local keywords).

[herbelin]

As suggested by the discussion in #17589, the question is raised of how technical we should be about detection of symbols which have to be declared as keywords for the grammar engine we use.

For instance, an alternative direction could be to support more backtracking in the parsing engine.