Upstreaming improvements?

[brandenburg]

Hi all,

we recently added a few improvements to the vendored version of CoqdocJS included in PROSA.

1. Updates to the style sheet, in particular to use Inconsolata as the font for code.
2. Ability to do unicode replacement for things that coqdoc emits non-atomically.
3. Replacement of common MatchComp syntax (boolean operators like &&, bigop like \sum, \in, etc.). This depends on (2).
4. Consider variables in binders for unicode replacement.
5. Use unicode italics for single-letter variables (e.g., i ➔ 𝘪).
6. Extended subscript detection.
7. Allow for (** comments in folded proofs.
8. Include the web fonts in the repo, to avoid leaking IP addresses of visitors to Google (we're forced to do this for GDPR compliance).

You can see examples of all this in action in the PROSA spec:

• a lemma with MathComp unicode replacements
• coqdoc comments in a folded proof

If there is interest in any of this, I would be happy to submit PRs to upstream the changes. Please let me know if you would consider merging this.