Fix rocqwc on tactics that end in Proof

[JoJoDeveloping]

The issue is fixed by making sure to not give any special treatment to the "Proof" keyword after seeing it the first time.

Closes #21422

I think that rocq wc is mostly undocumented, so I am not sure how to handle the yet-unchecked boxes. I am also not sure this requires adding to the changelog.

• Added / updated test-suite.

• Added changelog.
• Added / updated documentation.
  • Documented any new / changed user messages.
  • Updated documented syntax by running make doc_gram_rsts.

[coqbot-app]

Hello, thanks for your pull request!
In the future, we strongly recommend that you do not use master as the name of your branch when submitting a pull request.
By the way, you may be interested in reading our contributing guide.

[SkySkimmer]

Any @rocq-prover/coqdoc-maintainers can handle this?

[Lysxia]

• I think it's worth recording this in the changelog, in the 09-cli-tools section.

• For the sake of a smaller diff, I would prefer a solution that extends the character rule with one that consumes a whole word. And only doing that for the proof lexer is fine (until someone complains about the other cases).

[JoJoDeveloping]

I would prefer a solution that extends the character rule with one that consumes a whole word.

I can't figure out what you mean by this or how it's related to making the diff smaller for this PR 🙈

[JoJoDeveloping]

I added a changelog. I did not test that the added changelog entry works correctly because I could not get the documentation to build. If CI fails I would appreciate help here.