Unescaped Markdown #605
Description
The documentation for the option pp.mvars includes:
(pretty printer) display names of metavariables when true, and otherwise display them as '?_' (for expression metavariables) and as '_' (for universe level metavariables)
Except it's actually rendered as:
(pretty printer) display names of metavariables when true, and otherwise display them as '?' (for expression metavariables) and as '' (for universe level metavariables)
Because the _ characters are unescaped and interpreted as Markdown italics.
While this text can be found here in the docs, the source that needs to be fixed is actually in (multiple???) other repos.