From 8b58b887a95f0abfac16e8dc6f5e68f21e99ef31 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Sun, 16 Feb 2020 13:17:20 -0800
Subject: Show apostrophes and backticks in HTML, too.

---
 doc/tools/coqrst/notations/sphinx.py | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/doc/tools/coqrst/notations/sphinx.py b/doc/tools/coqrst/notations/sphinx.py
index ab18d136b8..5659a64b84 100644
--- a/doc/tools/coqrst/notations/sphinx.py
+++ b/doc/tools/coqrst/notations/sphinx.py
@@ -80,9 +80,11 @@ class TacticNotationsToSphinxVisitor(TacticNotationsVisitor):
         while atom != "":
             if atom[0] == "'":
                 node += nodes.raw("\\textquotesingle{}", "\\textquotesingle{}", format="latex")
+                node += nodes.raw("'", "'", format="html")
                 atom = atom[1:]
             elif atom[0] == "`":
                 node += nodes.raw("\\`{}", "\\`{}", format="latex")
+                node += nodes.raw("`", "`", format="html")
                 atom = atom[1:]
             else:
                 index_ap = atom.find("'")
-- 
cgit v1.2.3