Adapt w.r.t coq/coq#20167.

[ppedrot]

This is backwards compatible.

I copied the function here because Tok.equal in Coq is actually not the equality function, there is special-casing of KEYWORD and IDENT that used to be there to support a hack in the parser.

[ppedrot]

I'm not sure why the CI is still broken here, but it should really be backwards compatible, I tested it locally.

[SkySkimmer]

The CI for master seems to have issues with the stdlib split or renaming

Error: I don't know about package coq-stdlib (passed through --only-packages)

CI for <9.0 correctly says

Error (warning 8 [partial-match]): this pattern-matching is not exhaustive.
Here is an example of a case that is not matched:
(PATTERNIDENT _, _)

[gares]

What is Tok.equal then, and why it is called like that?

[ppedrot]

@gares it was introduced for backward compatibility with camlp4 quite a long time ago, and this IDENT ≤ KEYWORD rule was added to work around the fact that an indent could be turned at any point into a keyword. So that's a plain hack.

[ppedrot]

Anyone merging this?

[SkySkimmer]

This branch has conflicts that must be resolved

[ppedrot]

Rebased.

[SkySkimmer]

You still have the non exhaustive match issue on older Coq versions

[ppedrot]

Hopefully this does not trigger warnings or something.