[Sphinx] Add a few grammar constructions

Code from Paul Steckler (MIT).

12 files changed, 243 insertions, 111 deletions

diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 18f32d7a8..663ab9d37 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -28,8 +28,10 @@ from docutils.parsers.rst.directives.admonitions import BaseAdmonition
 from sphinx import addnodes
 from sphinx.roles import XRefRole
 from sphinx.util.nodes import set_source_info, set_role_source_info, make_refnode
+from sphinx.util.logging import getLogger
 from sphinx.directives import ObjectDescription
 from sphinx.domains import Domain, ObjType, Index
+from sphinx.domains.std import token_xrefs
 from sphinx.ext.mathbase import MathDirective, displaymath
 
 from . import coqdoc
@@ -155,6 +157,9 @@ class CoqObject(ObjectDescription):
         """Create a target and an index entry for name"""
         if name:
             target = self._add_target(signode, name)
+            # remove trailing . , found in commands, but not ... (ellipsis)
+            if name[-1] == "." and not name[-3:] == "..." :
+                name = name[0:-1]
             self._add_index_entry(name, target)
             return target
 
@@ -173,19 +178,19 @@ class NotationObject(CoqObject):
 class TacticObject(PlainObject):
     """An object to represent Coq tactics"""
     subdomain = "tac"
-    index_suffix = "(tactic)"
+    index_suffix = "(tac)"
     annotation = None
 
 class GallinaObject(PlainObject):
     """An object to represent Coq theorems"""
     subdomain = "thm"
-    index_suffix = "(theorem)"
+    index_suffix = "(thm)"
     annotation = "Theorem"
 
 class VernacObject(NotationObject):
     """An object to represent Coq commands"""
     subdomain = "cmd"
-    index_suffix = "(command)"
+    index_suffix = "(cmd)"
     annotation = "Command"
 
     def _name_from_signature(self, signature):
@@ -193,33 +198,72 @@ class VernacObject(NotationObject):
 
 class VernacVariantObject(VernacObject):
     """An object to represent variants of Coq commands"""
-    index_suffix = "(command variant)"
+    index_suffix = "(cmdv)"
     annotation = "Variant"
 
 class TacticNotationObject(NotationObject):
     """An object to represent Coq tactic notations"""
     subdomain = "tacn"
-    index_suffix = "(tactic notation)"
+    index_suffix = "(tacn)"
     annotation = None
 
 class TacticNotationVariantObject(TacticNotationObject):
     """An object to represent variants of Coq tactic notations"""
-    index_suffix = "(tactic variant)"
+    index_suffix = "(tacnv)"
     annotation = "Variant"
 
 class OptionObject(NotationObject):
-    """An object to represent variants of Coq options"""
+    """An object to represent Coq options"""
     subdomain = "opt"
-    index_suffix = "(option)"
+    index_suffix = "(opt)"
     annotation = "Option"
 
     def _name_from_signature(self, signature):
         return stringify_with_ellipses(signature)
 
+class ProductionObject(NotationObject):
+    """An object to represent grammar productions"""
+    subdomain = "prodn"
+    index_suffix = None
+    annotation = None
+
+    # override to create link targets for production left-hand sides
+    def run(self):
+        env = self.state.document.settings.env
+        objects = env.domaindata['std']['objects']
+
+        class ProdnError(Exception):
+            """Exception for ill-formed prodn"""
+            pass
+
+        [idx, node] = super().run()
+        try:
+            # find LHS of production
+            inline_lhs = node[0][0][0][0]  # may be fragile !!!
+            lhs_str = str(inline_lhs)
+            if lhs_str[0:7] != "<inline":
+                raise ProdnError("Expected atom on LHS")
+            lhs = inline_lhs[0]
+            # register link target
+            subnode = addnodes.production()
+            subnode['tokenname'] = lhs
+            idname = 'grammar-token-%s' % subnode['tokenname']
+            if idname not in self.state.document.ids:
+                subnode['ids'].append(idname)
+            self.state.document.note_implicit_target(subnode, subnode)
+            objects['token', subnode['tokenname']] = env.docname, idname
+            subnode.extend(token_xrefs(lhs))
+            # patch in link target
+            inline_lhs['ids'].append(idname)
+        except ProdnError as err:
+            getLogger(__name__).warning("Could not create link target for prodn: " + str(err) +
+                                        "\nSphinx represents the prodn as: " + str(node) + "\n")
+        return [idx, node]
+
 class ExceptionObject(NotationObject):
     """An object to represent Coq errors."""
     subdomain = "exn"
-    index_suffix = "(error)"
+    index_suffix = "(err)"
     annotation = "Error"
     # Uses “exn” since “err” already is a CSS class added by “writer_aux”.
 
@@ -371,6 +415,7 @@ class InferenceDirective(Directive):
     required_arguments = 1
     optional_arguments = 0
     has_content = True
+    final_argument_whitespace = True
 
     def make_math_node(self, latex):
         node = displaymath()
@@ -601,11 +646,13 @@ class CoqOptionIndex(CoqSubdomainsIndex):
 class CoqGallinaIndex(CoqSubdomainsIndex):
     name, localname, shortname, subdomains = "thmindex", "Gallina Index", "theorems", ["thm"]
 
-class CoqExceptionIndex(CoqSubdomainsIndex):
-    name, localname, shortname, subdomains = "exnindex", "Error Index", "errors", ["exn"]
+# we specify an index to make productions fit into the framework of notations
+# but not likely to include a link to this index
+class CoqProductionIndex(CoqSubdomainsIndex):
+    name, localname, shortname, subdomains = "prodnindex", "Production Index", "productions", ["prodn"]
 
-class CoqWarningIndex(CoqSubdomainsIndex):
-    name, localname, shortname, subdomains = "warnindex", "Warning Index", "warnings", ["warn"]
+class CoqExceptionIndex(CoqSubdomainsIndex):
+    name, localname, shortname, subdomains = "exnindex", "Errors and Warnings Index", "errors", ["exn", "warn"]
 
 class IndexXRefRole(XRefRole):
     """A link to one of our domain-specific indices."""
@@ -664,8 +711,9 @@ class CoqDomain(Domain):
         'tacv': ObjType('tacv', 'tacn'),
         'opt': ObjType('opt', 'opt'),
         'thm': ObjType('thm', 'thm'),
+        'prodn': ObjType('prodn', 'prodn'),
         'exn': ObjType('exn', 'exn'),
-        'warn': ObjType('warn', 'warn'),
+        'warn': ObjType('warn', 'exn'),
         'index': ObjType('index', 'index', searchprio=-1)
     }
 
@@ -680,6 +728,7 @@ class CoqDomain(Domain):
         'tacv': TacticNotationVariantObject,
         'opt': OptionObject,
         'thm': GallinaObject,
+        'prodn' : ProductionObject,
         'exn': ExceptionObject,
         'warn': WarningObject,
     }
@@ -691,6 +740,7 @@ class CoqDomain(Domain):
         'tacn': XRefRole(),
         'opt': XRefRole(),
         'thm': XRefRole(),
+        'prodn' : XRefRole(),
         'exn': XRefRole(),
         'warn': XRefRole(),
         # This one is special
@@ -704,7 +754,7 @@ class CoqDomain(Domain):
         'l': LtacRole, #FIXME unused?
     }
 
-    indices = [CoqVernacIndex, CoqTacticIndex, CoqOptionIndex, CoqGallinaIndex, CoqExceptionIndex, CoqWarningIndex]
+    indices = [CoqVernacIndex, CoqTacticIndex, CoqOptionIndex, CoqGallinaIndex, CoqProductionIndex, CoqExceptionIndex]
 
     data_version = 1
     initial_data = {
@@ -716,6 +766,7 @@ class CoqDomain(Domain):
             'tacn': {},
             'opt': {},
             'thm': {},
+            'prodn' : {},
             'exn': {},
             'warn': {},
         }
@@ -807,6 +858,7 @@ def setup(app):
     app.connect('doctree-resolved', simplify_source_code_blocks_for_latex)
 
     # Add extra styles
+    app.add_stylesheet("fonts.css")
     app.add_stylesheet("ansi.css")
     app.add_stylesheet("coqdoc.css")
     app.add_javascript("notations.js")
diff --git a/doc/tools/coqrst/notations/TacticNotations.g b/doc/tools/coqrst/notations/TacticNotations.g
index 72ae8eb6b..5176c51d2 100644
--- a/doc/tools/coqrst/notations/TacticNotations.g
+++ b/doc/tools/coqrst/notations/TacticNotations.g
@@ -15,16 +15,18 @@ grammar TacticNotations;
 
 top: blocks EOF;
 blocks: block ((whitespace)? block)*;
-block: atomic | hole | repeat | curlies;
+block: atomic | meta | hole | repeat | curlies;
 repeat: LGROUP (ATOM)? WHITESPACE blocks (WHITESPACE)? RBRACE;
 curlies: LBRACE (whitespace)? blocks (whitespace)? RBRACE;
 whitespace: WHITESPACE;
+meta: METACHAR;
 atomic: ATOM;
 hole: ID;
 
 LGROUP: '{' [+*?];
 LBRACE: '{';
 RBRACE: '}';
-ATOM: ~[@{} ]+;
+METACHAR: '%' [|()];
+ATOM: '@' | ~[@{} ]+;
 ID: '@' [a-zA-Z0-9_]+;
 WHITESPACE: ' '+;
diff --git a/doc/tools/coqrst/notations/TacticNotations.tokens b/doc/tools/coqrst/notations/TacticNotations.tokens
index 4d41a3883..76ed2b065 100644
--- a/doc/tools/coqrst/notations/TacticNotations.tokens
+++ b/doc/tools/coqrst/notations/TacticNotations.tokens
@@ -1,8 +1,9 @@
 LGROUP=1
 LBRACE=2
 RBRACE=3
-ATOM=4
-ID=5
-WHITESPACE=6
+METACHAR=4
+ATOM=5
+ID=6
+WHITESPACE=7
 '{'=2
 '}'=3
diff --git a/doc/tools/coqrst/notations/TacticNotationsLexer.py b/doc/tools/coqrst/notations/TacticNotationsLexer.py
index 4cac071ac..ffa774b9b 100644
--- a/doc/tools/coqrst/notations/TacticNotationsLexer.py
+++ b/doc/tools/coqrst/notations/TacticNotationsLexer.py
@@ -7,21 +7,24 @@ import sys
 
 def serializedATN():
     with StringIO() as buf:
-        buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\2\b")
-        buf.write("&\b\1\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7")
-        buf.write("\3\2\3\2\3\2\3\3\3\3\3\4\3\4\3\5\6\5\30\n\5\r\5\16\5\31")
-        buf.write("\3\6\3\6\6\6\36\n\6\r\6\16\6\37\3\7\6\7#\n\7\r\7\16\7")
-        buf.write("$\2\2\b\3\3\5\4\7\5\t\6\13\7\r\b\3\2\5\4\2,-AA\6\2\"\"")
-        buf.write("BB}}\177\177\6\2\62;C\\aac|\2(\2\3\3\2\2\2\2\5\3\2\2\2")
-        buf.write("\2\7\3\2\2\2\2\t\3\2\2\2\2\13\3\2\2\2\2\r\3\2\2\2\3\17")
-        buf.write("\3\2\2\2\5\22\3\2\2\2\7\24\3\2\2\2\t\27\3\2\2\2\13\33")
-        buf.write("\3\2\2\2\r\"\3\2\2\2\17\20\7}\2\2\20\21\t\2\2\2\21\4\3")
-        buf.write("\2\2\2\22\23\7}\2\2\23\6\3\2\2\2\24\25\7\177\2\2\25\b")
-        buf.write("\3\2\2\2\26\30\n\3\2\2\27\26\3\2\2\2\30\31\3\2\2\2\31")
-        buf.write("\27\3\2\2\2\31\32\3\2\2\2\32\n\3\2\2\2\33\35\7B\2\2\34")
-        buf.write("\36\t\4\2\2\35\34\3\2\2\2\36\37\3\2\2\2\37\35\3\2\2\2")
-        buf.write("\37 \3\2\2\2 \f\3\2\2\2!#\7\"\2\2\"!\3\2\2\2#$\3\2\2\2")
-        buf.write("$\"\3\2\2\2$%\3\2\2\2%\16\3\2\2\2\6\2\31\37$\2")
+        buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\2\t")
+        buf.write(".\b\1\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7")
+        buf.write("\4\b\t\b\3\2\3\2\3\2\3\3\3\3\3\4\3\4\3\5\3\5\3\5\3\6\3")
+        buf.write("\6\6\6\36\n\6\r\6\16\6\37\5\6\"\n\6\3\7\3\7\6\7&\n\7\r")
+        buf.write("\7\16\7\'\3\b\6\b+\n\b\r\b\16\b,\2\2\t\3\3\5\4\7\5\t\6")
+        buf.write("\13\7\r\b\17\t\3\2\6\4\2,-AA\4\2*+~~\6\2\"\"BB}}\177\177")
+        buf.write("\6\2\62;C\\aac|\2\61\2\3\3\2\2\2\2\5\3\2\2\2\2\7\3\2\2")
+        buf.write("\2\2\t\3\2\2\2\2\13\3\2\2\2\2\r\3\2\2\2\2\17\3\2\2\2\3")
+        buf.write("\21\3\2\2\2\5\24\3\2\2\2\7\26\3\2\2\2\t\30\3\2\2\2\13")
+        buf.write("!\3\2\2\2\r#\3\2\2\2\17*\3\2\2\2\21\22\7}\2\2\22\23\t")
+        buf.write("\2\2\2\23\4\3\2\2\2\24\25\7}\2\2\25\6\3\2\2\2\26\27\7")
+        buf.write("\177\2\2\27\b\3\2\2\2\30\31\7\'\2\2\31\32\t\3\2\2\32\n")
+        buf.write("\3\2\2\2\33\"\7B\2\2\34\36\n\4\2\2\35\34\3\2\2\2\36\37")
+        buf.write("\3\2\2\2\37\35\3\2\2\2\37 \3\2\2\2 \"\3\2\2\2!\33\3\2")
+        buf.write("\2\2!\35\3\2\2\2\"\f\3\2\2\2#%\7B\2\2$&\t\5\2\2%$\3\2")
+        buf.write("\2\2&\'\3\2\2\2\'%\3\2\2\2\'(\3\2\2\2(\16\3\2\2\2)+\7")
+        buf.write("\"\2\2*)\3\2\2\2+,\3\2\2\2,*\3\2\2\2,-\3\2\2\2-\20\3\2")
+        buf.write("\2\2\7\2\37!\',\2")
         return buf.getvalue()
 
 
@@ -34,9 +37,10 @@ class TacticNotationsLexer(Lexer):
     LGROUP = 1
     LBRACE = 2
     RBRACE = 3
-    ATOM = 4
-    ID = 5
-    WHITESPACE = 6
+    METACHAR = 4
+    ATOM = 5
+    ID = 6
+    WHITESPACE = 7
 
     channelNames = [ u"DEFAULT_TOKEN_CHANNEL", u"HIDDEN" ]
 
@@ -46,9 +50,10 @@ class TacticNotationsLexer(Lexer):
             "'{'", "'}'" ]
 
     symbolicNames = [ "<INVALID>",
-            "LGROUP", "LBRACE", "RBRACE", "ATOM", "ID", "WHITESPACE" ]
+            "LGROUP", "LBRACE", "RBRACE", "METACHAR", "ATOM", "ID", "WHITESPACE" ]
 
-    ruleNames = [ "LGROUP", "LBRACE", "RBRACE", "ATOM", "ID", "WHITESPACE" ]
+    ruleNames = [ "LGROUP", "LBRACE", "RBRACE", "METACHAR", "ATOM", "ID",
+                  "WHITESPACE" ]
 
     grammarFileName = "TacticNotations.g"
 
diff --git a/doc/tools/coqrst/notations/TacticNotationsLexer.tokens b/doc/tools/coqrst/notations/TacticNotationsLexer.tokens
index 4d41a3883..76ed2b065 100644
--- a/doc/tools/coqrst/notations/TacticNotationsLexer.tokens
+++ b/doc/tools/coqrst/notations/TacticNotationsLexer.tokens
@@ -1,8 +1,9 @@
 LGROUP=1
 LBRACE=2
 RBRACE=3
-ATOM=4
-ID=5
-WHITESPACE=6
+METACHAR=4
+ATOM=5
+ID=6
+WHITESPACE=7
 '{'=2
 '}'=3
diff --git a/doc/tools/coqrst/notations/TacticNotationsParser.py b/doc/tools/coqrst/notations/TacticNotationsParser.py
index 357902ddb..c7e28af52 100644
--- a/doc/tools/coqrst/notations/TacticNotationsParser.py
+++ b/doc/tools/coqrst/notations/TacticNotationsParser.py
@@ -7,28 +7,29 @@ import sys
 
 def serializedATN():
     with StringIO() as buf:
-        buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\3\b")
-        buf.write("A\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7\4\b")
-        buf.write("\t\b\4\t\t\t\3\2\3\2\3\2\3\3\3\3\5\3\30\n\3\3\3\7\3\33")
-        buf.write("\n\3\f\3\16\3\36\13\3\3\4\3\4\3\4\3\4\5\4$\n\4\3\5\3\5")
-        buf.write("\5\5(\n\5\3\5\3\5\3\5\5\5-\n\5\3\5\3\5\3\6\3\6\5\6\63")
-        buf.write("\n\6\3\6\3\6\5\6\67\n\6\3\6\3\6\3\7\3\7\3\b\3\b\3\t\3")
-        buf.write("\t\3\t\2\2\n\2\4\6\b\n\f\16\20\2\2\2A\2\22\3\2\2\2\4\25")
-        buf.write("\3\2\2\2\6#\3\2\2\2\b%\3\2\2\2\n\60\3\2\2\2\f:\3\2\2\2")
-        buf.write("\16<\3\2\2\2\20>\3\2\2\2\22\23\5\4\3\2\23\24\7\2\2\3\24")
-        buf.write("\3\3\2\2\2\25\34\5\6\4\2\26\30\5\f\7\2\27\26\3\2\2\2\27")
-        buf.write("\30\3\2\2\2\30\31\3\2\2\2\31\33\5\6\4\2\32\27\3\2\2\2")
-        buf.write("\33\36\3\2\2\2\34\32\3\2\2\2\34\35\3\2\2\2\35\5\3\2\2")
-        buf.write("\2\36\34\3\2\2\2\37$\5\16\b\2 $\5\20\t\2!$\5\b\5\2\"$")
-        buf.write("\5\n\6\2#\37\3\2\2\2# \3\2\2\2#!\3\2\2\2#\"\3\2\2\2$\7")
-        buf.write("\3\2\2\2%\'\7\3\2\2&(\7\6\2\2\'&\3\2\2\2\'(\3\2\2\2()")
-        buf.write("\3\2\2\2)*\7\b\2\2*,\5\4\3\2+-\7\b\2\2,+\3\2\2\2,-\3\2")
-        buf.write("\2\2-.\3\2\2\2./\7\5\2\2/\t\3\2\2\2\60\62\7\4\2\2\61\63")
-        buf.write("\5\f\7\2\62\61\3\2\2\2\62\63\3\2\2\2\63\64\3\2\2\2\64")
-        buf.write("\66\5\4\3\2\65\67\5\f\7\2\66\65\3\2\2\2\66\67\3\2\2\2")
-        buf.write("\678\3\2\2\289\7\5\2\29\13\3\2\2\2:;\7\b\2\2;\r\3\2\2")
-        buf.write("\2<=\7\6\2\2=\17\3\2\2\2>?\7\7\2\2?\21\3\2\2\2\t\27\34")
-        buf.write("#\',\62\66")
+        buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\3\t")
+        buf.write("F\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7\4\b")
+        buf.write("\t\b\4\t\t\t\4\n\t\n\3\2\3\2\3\2\3\3\3\3\5\3\32\n\3\3")
+        buf.write("\3\7\3\35\n\3\f\3\16\3 \13\3\3\4\3\4\3\4\3\4\3\4\5\4\'")
+        buf.write("\n\4\3\5\3\5\5\5+\n\5\3\5\3\5\3\5\5\5\60\n\5\3\5\3\5\3")
+        buf.write("\6\3\6\5\6\66\n\6\3\6\3\6\5\6:\n\6\3\6\3\6\3\7\3\7\3\b")
+        buf.write("\3\b\3\t\3\t\3\n\3\n\3\n\2\2\13\2\4\6\b\n\f\16\20\22\2")
+        buf.write("\2\2F\2\24\3\2\2\2\4\27\3\2\2\2\6&\3\2\2\2\b(\3\2\2\2")
+        buf.write("\n\63\3\2\2\2\f=\3\2\2\2\16?\3\2\2\2\20A\3\2\2\2\22C\3")
+        buf.write("\2\2\2\24\25\5\4\3\2\25\26\7\2\2\3\26\3\3\2\2\2\27\36")
+        buf.write("\5\6\4\2\30\32\5\f\7\2\31\30\3\2\2\2\31\32\3\2\2\2\32")
+        buf.write("\33\3\2\2\2\33\35\5\6\4\2\34\31\3\2\2\2\35 \3\2\2\2\36")
+        buf.write("\34\3\2\2\2\36\37\3\2\2\2\37\5\3\2\2\2 \36\3\2\2\2!\'")
+        buf.write("\5\20\t\2\"\'\5\16\b\2#\'\5\22\n\2$\'\5\b\5\2%\'\5\n\6")
+        buf.write("\2&!\3\2\2\2&\"\3\2\2\2&#\3\2\2\2&$\3\2\2\2&%\3\2\2\2")
+        buf.write("\'\7\3\2\2\2(*\7\3\2\2)+\7\7\2\2*)\3\2\2\2*+\3\2\2\2+")
+        buf.write(",\3\2\2\2,-\7\t\2\2-/\5\4\3\2.\60\7\t\2\2/.\3\2\2\2/\60")
+        buf.write("\3\2\2\2\60\61\3\2\2\2\61\62\7\5\2\2\62\t\3\2\2\2\63\65")
+        buf.write("\7\4\2\2\64\66\5\f\7\2\65\64\3\2\2\2\65\66\3\2\2\2\66")
+        buf.write("\67\3\2\2\2\679\5\4\3\28:\5\f\7\298\3\2\2\29:\3\2\2\2")
+        buf.write(":;\3\2\2\2;<\7\5\2\2<\13\3\2\2\2=>\7\t\2\2>\r\3\2\2\2")
+        buf.write("?@\7\6\2\2@\17\3\2\2\2AB\7\7\2\2B\21\3\2\2\2CD\7\b\2\2")
+        buf.write("D\23\3\2\2\2\t\31\36&*/\659")
         return buf.getvalue()
 
 
@@ -44,8 +45,8 @@ class TacticNotationsParser ( Parser ):
 
     literalNames = [ "<INVALID>", "<INVALID>", "'{'", "'}'" ]
 
-    symbolicNames = [ "<INVALID>", "LGROUP", "LBRACE", "RBRACE", "ATOM",
-                      "ID", "WHITESPACE" ]
+    symbolicNames = [ "<INVALID>", "LGROUP", "LBRACE", "RBRACE", "METACHAR",
+                      "ATOM", "ID", "WHITESPACE" ]
 
     RULE_top = 0
     RULE_blocks = 1
@@ -53,19 +54,21 @@ class TacticNotationsParser ( Parser ):
     RULE_repeat = 3
     RULE_curlies = 4
     RULE_whitespace = 5
-    RULE_atomic = 6
-    RULE_hole = 7
+    RULE_meta = 6
+    RULE_atomic = 7
+    RULE_hole = 8
 
     ruleNames =  [ "top", "blocks", "block", "repeat", "curlies", "whitespace",
-                   "atomic", "hole" ]
+                   "meta", "atomic", "hole" ]
 
     EOF = Token.EOF
     LGROUP=1
     LBRACE=2
     RBRACE=3
-    ATOM=4
-    ID=5
-    WHITESPACE=6
+    METACHAR=4
+    ATOM=5
+    ID=6
+    WHITESPACE=7
 
     def __init__(self, input:TokenStream, output:TextIO = sys.stdout):
         super().__init__(input, output)
@@ -106,9 +109,9 @@ class TacticNotationsParser ( Parser ):
         self.enterRule(localctx, 0, self.RULE_top)
         try:
             self.enterOuterAlt(localctx, 1)
-            self.state = 16
+            self.state = 18
             self.blocks()
-            self.state = 17
+            self.state = 19
             self.match(TacticNotationsParser.EOF)
         except RecognitionException as re:
             localctx.exception = re
@@ -157,24 +160,24 @@ class TacticNotationsParser ( Parser ):
         self._la = 0 # Token type
         try:
             self.enterOuterAlt(localctx, 1)
-            self.state = 19
+            self.state = 21
             self.block()
-            self.state = 26
+            self.state = 28
             self._errHandler.sync(self)
             _alt = self._interp.adaptivePredict(self._input,1,self._ctx)
             while _alt!=2 and _alt!=ATN.INVALID_ALT_NUMBER:
                 if _alt==1:
-                    self.state = 21
+                    self.state = 23
                     self._errHandler.sync(self)
                     _la = self._input.LA(1)
                     if _la==TacticNotationsParser.WHITESPACE:
-                        self.state = 20
+                        self.state = 22
                         self.whitespace()
 
 
-                    self.state = 23
+                    self.state = 25
                     self.block()
-                self.state = 28
+                self.state = 30
                 self._errHandler.sync(self)
                 _alt = self._interp.adaptivePredict(self._input,1,self._ctx)
 
@@ -196,6 +199,10 @@ class TacticNotationsParser ( Parser ):
             return self.getTypedRuleContext(TacticNotationsParser.AtomicContext,0)
 
 
+        def meta(self):
+            return self.getTypedRuleContext(TacticNotationsParser.MetaContext,0)
+
+
         def hole(self):
             return self.getTypedRuleContext(TacticNotationsParser.HoleContext,0)
 
@@ -225,27 +232,32 @@ class TacticNotationsParser ( Parser ):
         localctx = TacticNotationsParser.BlockContext(self, self._ctx, self.state)
         self.enterRule(localctx, 4, self.RULE_block)
         try:
-            self.state = 33
+            self.state = 36
             self._errHandler.sync(self)
             token = self._input.LA(1)
             if token in [TacticNotationsParser.ATOM]:
                 self.enterOuterAlt(localctx, 1)
-                self.state = 29
+                self.state = 31
                 self.atomic()
                 pass
-            elif token in [TacticNotationsParser.ID]:
+            elif token in [TacticNotationsParser.METACHAR]:
                 self.enterOuterAlt(localctx, 2)
-                self.state = 30
+                self.state = 32
+                self.meta()
+                pass
+            elif token in [TacticNotationsParser.ID]:
+                self.enterOuterAlt(localctx, 3)
+                self.state = 33
                 self.hole()
                 pass
             elif token in [TacticNotationsParser.LGROUP]:
-                self.enterOuterAlt(localctx, 3)
-                self.state = 31
+                self.enterOuterAlt(localctx, 4)
+                self.state = 34
                 self.repeat()
                 pass
             elif token in [TacticNotationsParser.LBRACE]:
-                self.enterOuterAlt(localctx, 4)
-                self.state = 32
+                self.enterOuterAlt(localctx, 5)
+                self.state = 35
                 self.curlies()
                 pass
             else:
@@ -303,29 +315,29 @@ class TacticNotationsParser ( Parser ):
         self._la = 0 # Token type
         try:
             self.enterOuterAlt(localctx, 1)
-            self.state = 35
+            self.state = 38
             self.match(TacticNotationsParser.LGROUP)
-            self.state = 37
+            self.state = 40
             self._errHandler.sync(self)
             _la = self._input.LA(1)
             if _la==TacticNotationsParser.ATOM:
-                self.state = 36
+                self.state = 39
                 self.match(TacticNotationsParser.ATOM)
 
 
-            self.state = 39
+            self.state = 42
             self.match(TacticNotationsParser.WHITESPACE)
-            self.state = 40
+            self.state = 43
             self.blocks()
-            self.state = 42
+            self.state = 45
             self._errHandler.sync(self)
             _la = self._input.LA(1)
             if _la==TacticNotationsParser.WHITESPACE:
-                self.state = 41
+                self.state = 44
                 self.match(TacticNotationsParser.WHITESPACE)
 
 
-            self.state = 44
+            self.state = 47
             self.match(TacticNotationsParser.RBRACE)
         except RecognitionException as re:
             localctx.exception = re
@@ -377,27 +389,27 @@ class TacticNotationsParser ( Parser ):
         self._la = 0 # Token type
         try:
             self.enterOuterAlt(localctx, 1)
-            self.state = 46
+            self.state = 49
             self.match(TacticNotationsParser.LBRACE)
-            self.state = 48
+            self.state = 51
             self._errHandler.sync(self)
             _la = self._input.LA(1)
             if _la==TacticNotationsParser.WHITESPACE:
-                self.state = 47
+                self.state = 50
                 self.whitespace()
 
 
-            self.state = 50
+            self.state = 53
             self.blocks()
-            self.state = 52
+            self.state = 55
             self._errHandler.sync(self)
             _la = self._input.LA(1)
             if _la==TacticNotationsParser.WHITESPACE:
-                self.state = 51
+                self.state = 54
                 self.whitespace()
 
 
-            self.state = 54
+            self.state = 57
             self.match(TacticNotationsParser.RBRACE)
         except RecognitionException as re:
             localctx.exception = re
@@ -434,7 +446,7 @@ class TacticNotationsParser ( Parser ):
         self.enterRule(localctx, 10, self.RULE_whitespace)
         try:
             self.enterOuterAlt(localctx, 1)
-            self.state = 56
+            self.state = 59
             self.match(TacticNotationsParser.WHITESPACE)
         except RecognitionException as re:
             localctx.exception = re
@@ -444,6 +456,43 @@ class TacticNotationsParser ( Parser ):
             self.exitRule()
         return localctx
 
+    class MetaContext(ParserRuleContext):
+
+        def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1):
+            super().__init__(parent, invokingState)
+            self.parser = parser
+
+        def METACHAR(self):
+            return self.getToken(TacticNotationsParser.METACHAR, 0)
+
+        def getRuleIndex(self):
+            return TacticNotationsParser.RULE_meta
+
+        def accept(self, visitor:ParseTreeVisitor):
+            if hasattr( visitor, "visitMeta" ):
+                return visitor.visitMeta(self)
+            else:
+                return visitor.visitChildren(self)
+
+
+
+
+    def meta(self):
+
+        localctx = TacticNotationsParser.MetaContext(self, self._ctx, self.state)
+        self.enterRule(localctx, 12, self.RULE_meta)
+        try:
+            self.enterOuterAlt(localctx, 1)
+            self.state = 61
+            self.match(TacticNotationsParser.METACHAR)
+        except RecognitionException as re:
+            localctx.exception = re
+            self._errHandler.reportError(self, re)
+            self._errHandler.recover(self, re)
+        finally:
+            self.exitRule()
+        return localctx
+
     class AtomicContext(ParserRuleContext):
 
         def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1):
@@ -468,10 +517,10 @@ class TacticNotationsParser ( Parser ):
     def atomic(self):
 
         localctx = TacticNotationsParser.AtomicContext(self, self._ctx, self.state)
-        self.enterRule(localctx, 12, self.RULE_atomic)
+        self.enterRule(localctx, 14, self.RULE_atomic)
         try:
             self.enterOuterAlt(localctx, 1)
-            self.state = 58
+            self.state = 63
             self.match(TacticNotationsParser.ATOM)
         except RecognitionException as re:
             localctx.exception = re
@@ -505,10 +554,10 @@ class TacticNotationsParser ( Parser ):
     def hole(self):
 
         localctx = TacticNotationsParser.HoleContext(self, self._ctx, self.state)
-        self.enterRule(localctx, 14, self.RULE_hole)
+        self.enterRule(localctx, 16, self.RULE_hole)
         try:
             self.enterOuterAlt(localctx, 1)
-            self.state = 60
+            self.state = 65
             self.match(TacticNotationsParser.ID)
         except RecognitionException as re:
             localctx.exception = re
diff --git a/doc/tools/coqrst/notations/TacticNotationsVisitor.py b/doc/tools/coqrst/notations/TacticNotationsVisitor.py
index 80e69d433..c0bcc4af3 100644
--- a/doc/tools/coqrst/notations/TacticNotationsVisitor.py
+++ b/doc/tools/coqrst/notations/TacticNotationsVisitor.py
@@ -39,6 +39,11 @@ class TacticNotationsVisitor(ParseTreeVisitor):
         return self.visitChildren(ctx)
 
 
+    # Visit a parse tree produced by TacticNotationsParser#meta.
+    def visitMeta(self, ctx:TacticNotationsParser.MetaContext):
+        return self.visitChildren(ctx)
+
+
     # Visit a parse tree produced by TacticNotationsParser#atomic.
     def visitAtomic(self, ctx:TacticNotationsParser.AtomicContext):
         return self.visitChildren(ctx)
@@ -50,4 +55,4 @@ class TacticNotationsVisitor(ParseTreeVisitor):
 
 
 
-del TacticNotationsParser
\ No newline at end of file
+del TacticNotationsParser
diff --git a/doc/tools/coqrst/notations/html.py b/doc/tools/coqrst/notations/html.py
index d91bbb64c..44212d788 100644
--- a/doc/tools/coqrst/notations/html.py
+++ b/doc/tools/coqrst/notations/html.py
@@ -42,6 +42,9 @@ class TacticNotationsToHTMLVisitor(TacticNotationsVisitor):
     def visitHole(self, ctx:TacticNotationsParser.HoleContext):
         tags.span(ctx.ID().getText()[1:], _class="hole")
 
+    def visitMeta(self, ctx:TacticNotationsParser.MetaContext):
+        tags.span(ctx.METACHAR().getText()[1:], _class="meta")
+
     def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext):
         tags.span(" ")          # TODO: no need for a <span> here
 
diff --git a/doc/tools/coqrst/notations/parsing.py b/doc/tools/coqrst/notations/parsing.py
index 73be6f26e..506240d90 100644
--- a/doc/tools/coqrst/notations/parsing.py
+++ b/doc/tools/coqrst/notations/parsing.py
@@ -12,7 +12,7 @@ from .TacticNotationsParser import TacticNotationsParser
 
 from antlr4 import CommonTokenStream, InputStream
 
-SUBSTITUTIONS = [("@bindings_list", "{+ (@id := @val) }"),
+SUBSTITUTIONS = [#("@bindings_list", "{+ (@id := @val) }"),
                  ("@qualid_or_string", "@id|@string")]
 
 def substitute(notation):
diff --git a/doc/tools/coqrst/notations/plain.py b/doc/tools/coqrst/notations/plain.py
index 5d4501892..f6e82fc68 100644
--- a/doc/tools/coqrst/notations/plain.py
+++ b/doc/tools/coqrst/notations/plain.py
@@ -41,6 +41,9 @@ class TacticNotationsToDotsVisitor(TacticNotationsVisitor):
     def visitHole(self, ctx:TacticNotationsParser.HoleContext):
         self.buffer.write("‘{}’".format(ctx.ID().getText()[1:]))
 
+    def visitMeta(self, ctx:TacticNotationsParser.MetaContext):
+        self.buffer.write(ctx.METACHAR().getText()[1:])
+
     def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext):
         self.buffer.write(" ")
 
diff --git a/doc/tools/coqrst/notations/regexp.py b/doc/tools/coqrst/notations/regexp.py
index cac6aaecb..ea820c719 100644
--- a/doc/tools/coqrst/notations/regexp.py
+++ b/doc/tools/coqrst/notations/regexp.py
@@ -47,6 +47,9 @@ class TacticNotationsToRegexpVisitor(TacticNotationsVisitor):
     def visitHole(self, ctx:TacticNotationsParser.HoleContext):
         self.buffer.write("([^();. \n]+)") # FIXME could allow more things
 
+    def visitMeta(self, ctx:TacticNotationsParser.MetaContext):
+        self.buffer.write(re.escape(ctx.METACHAR().getText()[1:]))
+
     def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext):
         self.buffer.write(r"\s+")
 
diff --git a/doc/tools/coqrst/notations/sphinx.py b/doc/tools/coqrst/notations/sphinx.py
index 889bf70a4..26a5f6968 100644
--- a/doc/tools/coqrst/notations/sphinx.py
+++ b/doc/tools/coqrst/notations/sphinx.py
@@ -20,6 +20,8 @@ from .TacticNotationsVisitor import TacticNotationsVisitor
 from docutils import nodes
 from sphinx import addnodes
 
+import sys
+
 class TacticNotationsToSphinxVisitor(TacticNotationsVisitor):
     def defaultResult(self):
         return []
@@ -62,6 +64,12 @@ class TacticNotationsToSphinxVisitor(TacticNotationsVisitor):
         node = nodes.inline(hole, token_name, classes=["hole"])
         return [addnodes.pending_xref(token_name, node, reftype='token', refdomain='std', reftarget=token_name)]
 
+    def visitMeta(self, ctx:TacticNotationsParser.MetaContext):
+        meta = ctx.METACHAR().getText()
+        metachar = meta[1:] # remove escape char
+        token_name = metachar
+        return [nodes.inline(metachar, token_name, classes=["meta"])]
+
     def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext):
         return [nodes.Text(" ")]