Dear Coq developers and contributors,
We’ve recently merged PR https://github.com/coq/coq/pull/14245.
This PR introduces a new requirement for PR authors, that will be checked in the linter. If your PR modifies the Coq syntax, then you will need to run the make doc_gram_rsts target (as documented in the updated PR template and in coq/README.md at master · coq/coq · GitHub) so that the documented syntax is updated.
Sometimes, this will also require editing doc/tools/docgram/common.edit_mlg, a file that contains a series of edits to get from Coq’s actual grammar to the documented grammar (various simplifications of implementation-specific details that are not worth getting in the documentation and renaming of some nonterminals for better readability).
If you encounter any difficulty, feel free to call @jfehrle or myself (@Zimmi48) for help.
Note that at the current time, there are still a few files which are not automatically updated when the syntax is changed. This includes the legacy Tactics chapter (which doesn’t contain as much content as before, because a lot of it has been moved to new pages), the Reasoning with Inductive Types chapter (we are currently in the process of updating / fixing the documented grammar in this chapter) and the SSR chapter. Still, the internal doc/tools/docgram/fullGrammar and doc/tools/docgram/orderedGrammar files should get updated for any change to the syntax (even if in some cases, the corresponding documentation will need to be manually updated).
We can answer any general questions in this thread as well.