test

[Alizter]

Description of the problem

No response

Small Coq file to reproduce the bug

If I put backticks in here does it mess things up?

example

### Version of Coq where this bug occurs

8.13.2

### Last version of Coq where the bug did not occur.

8.14+alpha

[Alizter]

Seems the answer is yes. I don't know if it will be too cluttered but perhaps put a note saying "Don't put backticks into the code box?". I also don't know how common this will be.

[Zimmi48]

(* No need to put code blocks markers *) in the placeholder maybe. Single backticks may be relevant Coq code, so we shouldn't just write "don't put backticks".

[Zimmi48]

Or maybe we should not do anything at first and change if we notice that people are getting confused.