aboutsummaryrefslogtreecommitdiff
path: root/doc/tools
diff options
context:
space:
mode:
Diffstat (limited to 'doc/tools')
-rw-r--r--doc/tools/coqrst/coqdomain.py8
1 files changed, 2 insertions, 6 deletions
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index b92c94fe2c..84f32e187b 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -34,7 +34,6 @@ from sphinx.util.logging import getLogger, get_node_location
from sphinx.directives import ObjectDescription
from sphinx.domains import Domain, ObjType, Index
from sphinx.domains.std import token_xrefs
-from sphinx.ext import mathbase
from . import coqdoc
from .repl import ansicolors
@@ -74,8 +73,7 @@ def make_target(objtype, targetid):
return "coq:{}.{}".format(objtype, targetid)
def make_math_node(latex, docname, nowrap):
- node = mathbase.displaymath()
- node['latex'] = latex
+ node = nodes.math_block(latex, latex)
node['label'] = None # Otherwise equations are numbered
node['nowrap'] = nowrap
node['docname'] = docname
@@ -493,9 +491,7 @@ class ProductionObject(CoqObject):
pass
def _target_id(self, name):
- # Use `name[1]` instead of ``nodes.make_id(name[1])`` to work around
- # https://github.com/sphinx-doc/sphinx/issues/4983
- return 'grammar-token-{}'.format(name[1])
+ return 'grammar-token-{}'.format(nodes.make_id(name[1]))
def _record_name(self, name, targetid):
env = self.state.document.settings.env