Proper RR typechecker

[yannl35133]

• Added / updated test-suite.

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

• Opened overlay pull requests.

[yannl35133]

It remains to be decided of what to do when the rule breaks SR: right now, coqc emits a warning but coqchk fails (hence the test failures)

[coqbot-app]

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

[coqbot-app]

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

[yannl35133]

@ppedrot The changes I introduce in commit 9adea52 conflict with your overwrite_structure function (environ.ml). I don't know how to solve them best, can you please take a look?
Basically, I introduce a new syntax for rewrite rules, which contains the same kind of information as constant_body. However, reduction machines still use the old machine_rewrite_rule syntax, so a translation is required. This translation requires an environment, and is required in your function.

[yannl35133]

I marked the PR as open for review, even though it fails to compile starting from commit 6.
The first 5 can be reviewed independently, they don't even talk of rewrite rules.
The 6th commit needs an answer from @ppedrot regarding his latest changes in environ.ml.