Extend editor language grammars provided by other extensions to support proof blocks

[andreadlm]

Extending the grammar for rocq provided by other language extensions (such as Coq-LSP) to include demonstration blocks could be useful for smoother user interaction.

Some questions remain open:

• It is unclear how it can be handled properly with only the injection mechanism between grammars.
• It is unclear whether multiple grammars for the same language, provided by different extensions can coexist (it seems not).
• It is unclear how to handle grammars that include references to scope names defined in other files.