aboutsummaryrefslogtreecommitdiff
path: root/doc/tools/coqrst
diff options
context:
space:
mode:
authorJim Fehrle2020-02-26 11:15:22 -0800
committerJim Fehrle2020-03-25 09:41:19 -0700
commite49cd002cb1ce6e06fec0e735bc6353c59416a6a (patch)
tree8b2015d2669c142f3c72b832978ae45fdebee828 /doc/tools/coqrst
parentbc70bb31c579b9482d0189f20806632c62b26a61 (diff)
Convert Gallina Extensions to use prodn
Diffstat (limited to 'doc/tools/coqrst')
-rw-r--r--doc/tools/coqrst/coqdomain.py2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 0b94b0d675..6332c4c81d 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -337,7 +337,7 @@ class TacticNotationObject(NotationObject):
"""
subdomain = "tacn"
index_suffix = "(tactic)"
- annotation = None
+ annotation = "Tactic"
class AttributeNotationObject(NotationObject):
"""An attribute.