[refman] Introduce syntax for alternatives in notations

Closes GH-8482.

10 files changed, 704 insertions, 205 deletions

diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 1784519f5f..4bdfac7c42 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -418,7 +418,7 @@ class ProductionObject(CoqObject):
     Example::
 
         .. prodn:: term += let: @pattern := @term in @term
-        .. prodn:: occ_switch ::= { {? + %| - } {* @num } }
+        .. prodn:: occ_switch ::= { {? {| + | - } } {* @num } }
 
     """
     subdomain = "prodn"
diff --git a/doc/tools/coqrst/notations/TacticNotations.g b/doc/tools/coqrst/notations/TacticNotations.g
index a889ebda7b..01c656eb23 100644
--- a/doc/tools/coqrst/notations/TacticNotations.g
+++ b/doc/tools/coqrst/notations/TacticNotations.g
@@ -13,21 +13,38 @@ grammar TacticNotations;
 // needs rendering (in particular whitespace (kept in output) vs. WHITESPACE
 // (discarded)).
 
+// The distinction between nopipeblock and block is needed because we only want
+// to require escaping within alternative blocks, so that e.g. `first [ x | y ]`
+// can be written without escaping the `|`.
+
 top: blocks EOF;
 blocks: block ((whitespace)? block)*;
-block: atomic | meta | hole | repeat | curlies;
-repeat: LGROUP (ATOM)? WHITESPACE blocks (WHITESPACE)? RBRACE;
+
+block: pipe | nopipeblock;
+nopipeblock: atomic | escaped | hole | alternative | repeat | curlies;
+
+alternative: LALT (WHITESPACE)? altblocks (WHITESPACE)? RBRACE;
+altblocks: altblock ((WHITESPACE)? altsep (WHITESPACE)? altblock)+;
+altblock: nopipeblock ((whitespace)? nopipeblock)*;
+
+repeat: LGROUP (ATOM | PIPE)? WHITESPACE blocks (WHITESPACE)? RBRACE;
 curlies: LBRACE (whitespace)? blocks (whitespace)? RBRACE;
+
+pipe: PIPE;
+altsep: PIPE;
 whitespace: WHITESPACE;
-meta: METACHAR;
+escaped: ESCAPED;
 atomic: ATOM (SUB)?;
 hole: ID (SUB)?;
 
-LGROUP: '{' [+*?];
+
+LALT: '{|';
+LGROUP: '{+' | '{*' | '{?';
 LBRACE: '{';
 RBRACE: '}';
-METACHAR: '%' [|(){}];
-ATOM: '@' | '_' | ~[@_{} ]+;
+ESCAPED: '%{' | '%}' | '%|';
+PIPE: '|';
+ATOM: '@' | '_' | ~[@_{}| ]+;
 ID: '@' ('_'? [a-zA-Z0-9])+;
 SUB: '_' '_' [a-zA-Z0-9]+;
 WHITESPACE: ' '+;
diff --git a/doc/tools/coqrst/notations/TacticNotations.tokens b/doc/tools/coqrst/notations/TacticNotations.tokens
index 88b38f97a6..2670e20aa6 100644
--- a/doc/tools/coqrst/notations/TacticNotations.tokens
+++ b/doc/tools/coqrst/notations/TacticNotations.tokens
@@ -1,10 +1,14 @@
-LGROUP=1
-LBRACE=2
-RBRACE=3
-METACHAR=4
-ATOM=5
-ID=6
-SUB=7
-WHITESPACE=8
-'{'=2
-'}'=3
+LALT=1
+LGROUP=2
+LBRACE=3
+RBRACE=4
+ESCAPED=5
+PIPE=6
+ATOM=7
+ID=8
+SUB=9
+WHITESPACE=10
+'{|'=1
+'{'=3
+'}'=4
+'|'=6
diff --git a/doc/tools/coqrst/notations/TacticNotationsLexer.py b/doc/tools/coqrst/notations/TacticNotationsLexer.py
index 27293e7e09..e3a115e32a 100644
--- a/doc/tools/coqrst/notations/TacticNotationsLexer.py
+++ b/doc/tools/coqrst/notations/TacticNotationsLexer.py
@@ -1,4 +1,4 @@
-# Generated from TacticNotations.g by ANTLR 4.7
+# Generated from TacticNotations.g by ANTLR 4.7.2
 from antlr4 import *
 from io import StringIO
 from typing.io import TextIO
@@ -7,28 +7,34 @@ import sys
 
 def serializedATN():
     with StringIO() as buf:
-        buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\2\n")
-        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\4\t\t\t\3\2\3\2\3\2\3\3\3\3\3\4\3\4\3\5\3\5\3")
-        buf.write("\5\3\6\3\6\6\6 \n\6\r\6\16\6!\5\6$\n\6\3\7\3\7\5\7(\n")
-        buf.write("\7\3\7\6\7+\n\7\r\7\16\7,\3\b\3\b\3\b\6\b\62\n\b\r\b\16")
-        buf.write("\b\63\3\t\6\t\67\n\t\r\t\16\t8\2\2\n\3\3\5\4\7\5\t\6\13")
-        buf.write("\7\r\b\17\t\21\n\3\2\7\4\2,-AA\4\2*+}\177\4\2BBaa\7\2")
-        buf.write("\"\"BBaa}}\177\177\5\2\62;C\\c|\2?\2\3\3\2\2\2\2\5\3\2")
-        buf.write("\2\2\2\7\3\2\2\2\2\t\3\2\2\2\2\13\3\2\2\2\2\r\3\2\2\2")
-        buf.write("\2\17\3\2\2\2\2\21\3\2\2\2\3\23\3\2\2\2\5\26\3\2\2\2\7")
-        buf.write("\30\3\2\2\2\t\32\3\2\2\2\13#\3\2\2\2\r%\3\2\2\2\17.\3")
-        buf.write("\2\2\2\21\66\3\2\2\2\23\24\7}\2\2\24\25\t\2\2\2\25\4\3")
-        buf.write("\2\2\2\26\27\7}\2\2\27\6\3\2\2\2\30\31\7\177\2\2\31\b")
-        buf.write("\3\2\2\2\32\33\7\'\2\2\33\34\t\3\2\2\34\n\3\2\2\2\35$")
-        buf.write("\t\4\2\2\36 \n\5\2\2\37\36\3\2\2\2 !\3\2\2\2!\37\3\2\2")
-        buf.write("\2!\"\3\2\2\2\"$\3\2\2\2#\35\3\2\2\2#\37\3\2\2\2$\f\3")
-        buf.write("\2\2\2%*\7B\2\2&(\7a\2\2\'&\3\2\2\2\'(\3\2\2\2()\3\2\2")
-        buf.write("\2)+\t\6\2\2*\'\3\2\2\2+,\3\2\2\2,*\3\2\2\2,-\3\2\2\2")
-        buf.write("-\16\3\2\2\2./\7a\2\2/\61\7a\2\2\60\62\t\6\2\2\61\60\3")
-        buf.write("\2\2\2\62\63\3\2\2\2\63\61\3\2\2\2\63\64\3\2\2\2\64\20")
-        buf.write("\3\2\2\2\65\67\7\"\2\2\66\65\3\2\2\2\678\3\2\2\28\66\3")
-        buf.write("\2\2\289\3\2\2\29\22\3\2\2\2\t\2!#\',\638\2")
+        buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\2\f")
+        buf.write("M\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\4\t\t\t\4\n\t\n\4\13\t\13\3\2\3\2\3\2\3\3\3\3")
+        buf.write("\3\3\3\3\3\3\3\3\5\3!\n\3\3\4\3\4\3\5\3\5\3\6\3\6\3\6")
+        buf.write("\3\6\3\6\3\6\5\6-\n\6\3\7\3\7\3\b\3\b\6\b\63\n\b\r\b\16")
+        buf.write("\b\64\5\b\67\n\b\3\t\3\t\5\t;\n\t\3\t\6\t>\n\t\r\t\16")
+        buf.write("\t?\3\n\3\n\3\n\6\nE\n\n\r\n\16\nF\3\13\6\13J\n\13\r\13")
+        buf.write("\16\13K\2\2\f\3\3\5\4\7\5\t\6\13\7\r\b\17\t\21\n\23\13")
+        buf.write("\25\f\3\2\5\4\2BBaa\6\2\"\"BBaa}\177\5\2\62;C\\c|\2V\2")
+        buf.write("\3\3\2\2\2\2\5\3\2\2\2\2\7\3\2\2\2\2\t\3\2\2\2\2\13\3")
+        buf.write("\2\2\2\2\r\3\2\2\2\2\17\3\2\2\2\2\21\3\2\2\2\2\23\3\2")
+        buf.write("\2\2\2\25\3\2\2\2\3\27\3\2\2\2\5 \3\2\2\2\7\"\3\2\2\2")
+        buf.write("\t$\3\2\2\2\13,\3\2\2\2\r.\3\2\2\2\17\66\3\2\2\2\218\3")
+        buf.write("\2\2\2\23A\3\2\2\2\25I\3\2\2\2\27\30\7}\2\2\30\31\7~\2")
+        buf.write("\2\31\4\3\2\2\2\32\33\7}\2\2\33!\7-\2\2\34\35\7}\2\2\35")
+        buf.write("!\7,\2\2\36\37\7}\2\2\37!\7A\2\2 \32\3\2\2\2 \34\3\2\2")
+        buf.write("\2 \36\3\2\2\2!\6\3\2\2\2\"#\7}\2\2#\b\3\2\2\2$%\7\177")
+        buf.write("\2\2%\n\3\2\2\2&\'\7\'\2\2\'-\7}\2\2()\7\'\2\2)-\7\177")
+        buf.write("\2\2*+\7\'\2\2+-\7~\2\2,&\3\2\2\2,(\3\2\2\2,*\3\2\2\2")
+        buf.write("-\f\3\2\2\2./\7~\2\2/\16\3\2\2\2\60\67\t\2\2\2\61\63\n")
+        buf.write("\3\2\2\62\61\3\2\2\2\63\64\3\2\2\2\64\62\3\2\2\2\64\65")
+        buf.write("\3\2\2\2\65\67\3\2\2\2\66\60\3\2\2\2\66\62\3\2\2\2\67")
+        buf.write("\20\3\2\2\28=\7B\2\29;\7a\2\2:9\3\2\2\2:;\3\2\2\2;<\3")
+        buf.write("\2\2\2<>\t\4\2\2=:\3\2\2\2>?\3\2\2\2?=\3\2\2\2?@\3\2\2")
+        buf.write("\2@\22\3\2\2\2AB\7a\2\2BD\7a\2\2CE\t\4\2\2DC\3\2\2\2E")
+        buf.write("F\3\2\2\2FD\3\2\2\2FG\3\2\2\2G\24\3\2\2\2HJ\7\"\2\2IH")
+        buf.write("\3\2\2\2JK\3\2\2\2KI\3\2\2\2KL\3\2\2\2L\26\3\2\2\2\13")
+        buf.write("\2 ,\64\66:?FK\2")
         return buf.getvalue()
 
 
@@ -38,34 +44,36 @@ class TacticNotationsLexer(Lexer):
 
     decisionsToDFA = [ DFA(ds, i) for i, ds in enumerate(atn.decisionToState) ]
 
-    LGROUP = 1
-    LBRACE = 2
-    RBRACE = 3
-    METACHAR = 4
-    ATOM = 5
-    ID = 6
-    SUB = 7
-    WHITESPACE = 8
+    LALT = 1
+    LGROUP = 2
+    LBRACE = 3
+    RBRACE = 4
+    ESCAPED = 5
+    PIPE = 6
+    ATOM = 7
+    ID = 8
+    SUB = 9
+    WHITESPACE = 10
 
     channelNames = [ u"DEFAULT_TOKEN_CHANNEL", u"HIDDEN" ]
 
     modeNames = [ "DEFAULT_MODE" ]
 
     literalNames = [ "<INVALID>",
-            "'{'", "'}'" ]
+            "'{|'", "'{'", "'}'", "'|'" ]
 
     symbolicNames = [ "<INVALID>",
-            "LGROUP", "LBRACE", "RBRACE", "METACHAR", "ATOM", "ID", "SUB",
-            "WHITESPACE" ]
+            "LALT", "LGROUP", "LBRACE", "RBRACE", "ESCAPED", "PIPE", "ATOM",
+            "ID", "SUB", "WHITESPACE" ]
 
-    ruleNames = [ "LGROUP", "LBRACE", "RBRACE", "METACHAR", "ATOM", "ID",
-                  "SUB", "WHITESPACE" ]
+    ruleNames = [ "LALT", "LGROUP", "LBRACE", "RBRACE", "ESCAPED", "PIPE",
+                  "ATOM", "ID", "SUB", "WHITESPACE" ]
 
     grammarFileName = "TacticNotations.g"
 
     def __init__(self, input=None, output:TextIO = sys.stdout):
         super().__init__(input, output)
-        self.checkVersion("4.7")
+        self.checkVersion("4.7.2")
         self._interp = LexerATNSimulator(self, self.atn, self.decisionsToDFA, PredictionContextCache())
         self._actions = None
         self._predicates = None
diff --git a/doc/tools/coqrst/notations/TacticNotationsLexer.tokens b/doc/tools/coqrst/notations/TacticNotationsLexer.tokens
index 88b38f97a6..2670e20aa6 100644
--- a/doc/tools/coqrst/notations/TacticNotationsLexer.tokens
+++ b/doc/tools/coqrst/notations/TacticNotationsLexer.tokens
@@ -1,10 +1,14 @@
-LGROUP=1
-LBRACE=2
-RBRACE=3
-METACHAR=4
-ATOM=5
-ID=6
-SUB=7
-WHITESPACE=8
-'{'=2
-'}'=3
+LALT=1
+LGROUP=2
+LBRACE=3
+RBRACE=4
+ESCAPED=5
+PIPE=6
+ATOM=7
+ID=8
+SUB=9
+WHITESPACE=10
+'{|'=1
+'{'=3
+'}'=4
+'|'=6
diff --git a/doc/tools/coqrst/notations/TacticNotationsParser.py b/doc/tools/coqrst/notations/TacticNotationsParser.py
index 645f078979..4a2a73672a 100644
--- a/doc/tools/coqrst/notations/TacticNotationsParser.py
+++ b/doc/tools/coqrst/notations/TacticNotationsParser.py
@@ -1,4 +1,4 @@
-# Generated from TacticNotations.g by ANTLR 4.7
+# Generated from TacticNotations.g by ANTLR 4.7.2
 # encoding: utf-8
 from antlr4 import *
 from io import StringIO
@@ -7,31 +7,47 @@ import sys
 
 def serializedATN():
     with StringIO() as buf:
-        buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\3\n")
-        buf.write("J\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\5\tD\n\t\3\n\3\n\5\nH\n\n\3\n\2\2\13\2\4")
-        buf.write("\6\b\n\f\16\20\22\2\2\2L\2\24\3\2\2\2\4\27\3\2\2\2\6&")
-        buf.write("\3\2\2\2\b(\3\2\2\2\n\63\3\2\2\2\f=\3\2\2\2\16?\3\2\2")
-        buf.write("\2\20A\3\2\2\2\22E\3\2\2\2\24\25\5\4\3\2\25\26\7\2\2\3")
-        buf.write("\26\3\3\2\2\2\27\36\5\6\4\2\30\32\5\f\7\2\31\30\3\2\2")
-        buf.write("\2\31\32\3\2\2\2\32\33\3\2\2\2\33\35\5\6\4\2\34\31\3\2")
-        buf.write("\2\2\35 \3\2\2\2\36\34\3\2\2\2\36\37\3\2\2\2\37\5\3\2")
-        buf.write("\2\2 \36\3\2\2\2!\'\5\20\t\2\"\'\5\16\b\2#\'\5\22\n\2")
-        buf.write("$\'\5\b\5\2%\'\5\n\6\2&!\3\2\2\2&\"\3\2\2\2&#\3\2\2\2")
-        buf.write("&$\3\2\2\2&%\3\2\2\2\'\7\3\2\2\2(*\7\3\2\2)+\7\7\2\2*")
-        buf.write(")\3\2\2\2*+\3\2\2\2+,\3\2\2\2,-\7\n\2\2-/\5\4\3\2.\60")
-        buf.write("\7\n\2\2/.\3\2\2\2/\60\3\2\2\2\60\61\3\2\2\2\61\62\7\5")
-        buf.write("\2\2\62\t\3\2\2\2\63\65\7\4\2\2\64\66\5\f\7\2\65\64\3")
-        buf.write("\2\2\2\65\66\3\2\2\2\66\67\3\2\2\2\679\5\4\3\28:\5\f\7")
-        buf.write("\298\3\2\2\29:\3\2\2\2:;\3\2\2\2;<\7\5\2\2<\13\3\2\2\2")
-        buf.write("=>\7\n\2\2>\r\3\2\2\2?@\7\6\2\2@\17\3\2\2\2AC\7\7\2\2")
-        buf.write("BD\7\t\2\2CB\3\2\2\2CD\3\2\2\2D\21\3\2\2\2EG\7\b\2\2F")
-        buf.write("H\7\t\2\2GF\3\2\2\2GH\3\2\2\2H\23\3\2\2\2\13\31\36&*/")
-        buf.write("\659CG")
+        buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\3\f")
+        buf.write("\u0081\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\4\t\t\t\4\n\t\n\4\13\t\13\4\f\t\f\4\r\t\r\4\16")
+        buf.write("\t\16\4\17\t\17\4\20\t\20\3\2\3\2\3\2\3\3\3\3\5\3&\n\3")
+        buf.write("\3\3\7\3)\n\3\f\3\16\3,\13\3\3\4\3\4\5\4\60\n\4\3\5\3")
+        buf.write("\5\3\5\3\5\3\5\3\5\5\58\n\5\3\6\3\6\5\6<\n\6\3\6\3\6\5")
+        buf.write("\6@\n\6\3\6\3\6\3\7\3\7\5\7F\n\7\3\7\3\7\5\7J\n\7\3\7")
+        buf.write("\3\7\6\7N\n\7\r\7\16\7O\3\b\3\b\5\bT\n\b\3\b\7\bW\n\b")
+        buf.write("\f\b\16\bZ\13\b\3\t\3\t\5\t^\n\t\3\t\3\t\3\t\5\tc\n\t")
+        buf.write("\3\t\3\t\3\n\3\n\5\ni\n\n\3\n\3\n\5\nm\n\n\3\n\3\n\3\13")
+        buf.write("\3\13\3\f\3\f\3\r\3\r\3\16\3\16\3\17\3\17\5\17{\n\17\3")
+        buf.write("\20\3\20\5\20\177\n\20\3\20\2\2\21\2\4\6\b\n\f\16\20\22")
+        buf.write("\24\26\30\32\34\36\2\3\3\2\b\t\2\u0086\2 \3\2\2\2\4#\3")
+        buf.write("\2\2\2\6/\3\2\2\2\b\67\3\2\2\2\n9\3\2\2\2\fC\3\2\2\2\16")
+        buf.write("Q\3\2\2\2\20[\3\2\2\2\22f\3\2\2\2\24p\3\2\2\2\26r\3\2")
+        buf.write("\2\2\30t\3\2\2\2\32v\3\2\2\2\34x\3\2\2\2\36|\3\2\2\2 ")
+        buf.write("!\5\4\3\2!\"\7\2\2\3\"\3\3\2\2\2#*\5\6\4\2$&\5\30\r\2")
+        buf.write("%$\3\2\2\2%&\3\2\2\2&\'\3\2\2\2\')\5\6\4\2(%\3\2\2\2)")
+        buf.write(",\3\2\2\2*(\3\2\2\2*+\3\2\2\2+\5\3\2\2\2,*\3\2\2\2-\60")
+        buf.write("\5\24\13\2.\60\5\b\5\2/-\3\2\2\2/.\3\2\2\2\60\7\3\2\2")
+        buf.write("\2\618\5\34\17\2\628\5\32\16\2\638\5\36\20\2\648\5\n\6")
+        buf.write("\2\658\5\20\t\2\668\5\22\n\2\67\61\3\2\2\2\67\62\3\2\2")
+        buf.write("\2\67\63\3\2\2\2\67\64\3\2\2\2\67\65\3\2\2\2\67\66\3\2")
+        buf.write("\2\28\t\3\2\2\29;\7\3\2\2:<\7\f\2\2;:\3\2\2\2;<\3\2\2")
+        buf.write("\2<=\3\2\2\2=?\5\f\7\2>@\7\f\2\2?>\3\2\2\2?@\3\2\2\2@")
+        buf.write("A\3\2\2\2AB\7\6\2\2B\13\3\2\2\2CM\5\16\b\2DF\7\f\2\2E")
+        buf.write("D\3\2\2\2EF\3\2\2\2FG\3\2\2\2GI\5\26\f\2HJ\7\f\2\2IH\3")
+        buf.write("\2\2\2IJ\3\2\2\2JK\3\2\2\2KL\5\16\b\2LN\3\2\2\2ME\3\2")
+        buf.write("\2\2NO\3\2\2\2OM\3\2\2\2OP\3\2\2\2P\r\3\2\2\2QX\5\b\5")
+        buf.write("\2RT\5\30\r\2SR\3\2\2\2ST\3\2\2\2TU\3\2\2\2UW\5\b\5\2")
+        buf.write("VS\3\2\2\2WZ\3\2\2\2XV\3\2\2\2XY\3\2\2\2Y\17\3\2\2\2Z")
+        buf.write("X\3\2\2\2[]\7\4\2\2\\^\t\2\2\2]\\\3\2\2\2]^\3\2\2\2^_")
+        buf.write("\3\2\2\2_`\7\f\2\2`b\5\4\3\2ac\7\f\2\2ba\3\2\2\2bc\3\2")
+        buf.write("\2\2cd\3\2\2\2de\7\6\2\2e\21\3\2\2\2fh\7\5\2\2gi\5\30")
+        buf.write("\r\2hg\3\2\2\2hi\3\2\2\2ij\3\2\2\2jl\5\4\3\2km\5\30\r")
+        buf.write("\2lk\3\2\2\2lm\3\2\2\2mn\3\2\2\2no\7\6\2\2o\23\3\2\2\2")
+        buf.write("pq\7\b\2\2q\25\3\2\2\2rs\7\b\2\2s\27\3\2\2\2tu\7\f\2\2")
+        buf.write("u\31\3\2\2\2vw\7\7\2\2w\33\3\2\2\2xz\7\t\2\2y{\7\13\2")
+        buf.write("\2zy\3\2\2\2z{\3\2\2\2{\35\3\2\2\2|~\7\n\2\2}\177\7\13")
+        buf.write("\2\2~}\3\2\2\2~\177\3\2\2\2\177\37\3\2\2\2\23%*/\67;?")
+        buf.write("EIOSX]bhlz~")
         return buf.getvalue()
 
 
@@ -45,37 +61,47 @@ class TacticNotationsParser ( Parser ):
 
     sharedContextCache = PredictionContextCache()
 
-    literalNames = [ "<INVALID>", "<INVALID>", "'{'", "'}'" ]
+    literalNames = [ "<INVALID>", "'{|'", "<INVALID>", "'{'", "'}'", "<INVALID>",
+                     "'|'" ]
 
-    symbolicNames = [ "<INVALID>", "LGROUP", "LBRACE", "RBRACE", "METACHAR",
-                      "ATOM", "ID", "SUB", "WHITESPACE" ]
+    symbolicNames = [ "<INVALID>", "LALT", "LGROUP", "LBRACE", "RBRACE",
+                      "ESCAPED", "PIPE", "ATOM", "ID", "SUB", "WHITESPACE" ]
 
     RULE_top = 0
     RULE_blocks = 1
     RULE_block = 2
-    RULE_repeat = 3
-    RULE_curlies = 4
-    RULE_whitespace = 5
-    RULE_meta = 6
-    RULE_atomic = 7
-    RULE_hole = 8
-
-    ruleNames =  [ "top", "blocks", "block", "repeat", "curlies", "whitespace",
-                   "meta", "atomic", "hole" ]
+    RULE_nopipeblock = 3
+    RULE_alternative = 4
+    RULE_altblocks = 5
+    RULE_altblock = 6
+    RULE_repeat = 7
+    RULE_curlies = 8
+    RULE_pipe = 9
+    RULE_altsep = 10
+    RULE_whitespace = 11
+    RULE_escaped = 12
+    RULE_atomic = 13
+    RULE_hole = 14
+
+    ruleNames =  [ "top", "blocks", "block", "nopipeblock", "alternative",
+                   "altblocks", "altblock", "repeat", "curlies", "pipe",
+                   "altsep", "whitespace", "escaped", "atomic", "hole" ]
 
     EOF = Token.EOF
-    LGROUP=1
-    LBRACE=2
-    RBRACE=3
-    METACHAR=4
-    ATOM=5
-    ID=6
-    SUB=7
-    WHITESPACE=8
+    LALT=1
+    LGROUP=2
+    LBRACE=3
+    RBRACE=4
+    ESCAPED=5
+    PIPE=6
+    ATOM=7
+    ID=8
+    SUB=9
+    WHITESPACE=10
 
     def __init__(self, input:TokenStream, output:TextIO = sys.stdout):
         super().__init__(input, output)
-        self.checkVersion("4.7")
+        self.checkVersion("4.7.2")
         self._interp = ParserATNSimulator(self, self.atn, self.decisionsToDFA, self.sharedContextCache)
         self._predicates = None
 
@@ -112,9 +138,9 @@ class TacticNotationsParser ( Parser ):
         self.enterRule(localctx, 0, self.RULE_top)
         try:
             self.enterOuterAlt(localctx, 1)
-            self.state = 18
+            self.state = 30
             self.blocks()
-            self.state = 19
+            self.state = 31
             self.match(TacticNotationsParser.EOF)
         except RecognitionException as re:
             localctx.exception = re
@@ -163,24 +189,24 @@ class TacticNotationsParser ( Parser ):
         self._la = 0 # Token type
         try:
             self.enterOuterAlt(localctx, 1)
-            self.state = 21
+            self.state = 33
             self.block()
-            self.state = 28
+            self.state = 40
             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 = 23
+                    self.state = 35
                     self._errHandler.sync(self)
                     _la = self._input.LA(1)
                     if _la==TacticNotationsParser.WHITESPACE:
-                        self.state = 22
+                        self.state = 34
                         self.whitespace()
 
 
-                    self.state = 25
+                    self.state = 37
                     self.block()
-                self.state = 30
+                self.state = 42
                 self._errHandler.sync(self)
                 _alt = self._interp.adaptivePredict(self._input,1,self._ctx)
 
@@ -198,18 +224,77 @@ class TacticNotationsParser ( Parser ):
             super().__init__(parent, invokingState)
             self.parser = parser
 
+        def pipe(self):
+            return self.getTypedRuleContext(TacticNotationsParser.PipeContext,0)
+
+
+        def nopipeblock(self):
+            return self.getTypedRuleContext(TacticNotationsParser.NopipeblockContext,0)
+
+
+        def getRuleIndex(self):
+            return TacticNotationsParser.RULE_block
+
+        def accept(self, visitor:ParseTreeVisitor):
+            if hasattr( visitor, "visitBlock" ):
+                return visitor.visitBlock(self)
+            else:
+                return visitor.visitChildren(self)
+
+
+
+
+    def block(self):
+
+        localctx = TacticNotationsParser.BlockContext(self, self._ctx, self.state)
+        self.enterRule(localctx, 4, self.RULE_block)
+        try:
+            self.state = 45
+            self._errHandler.sync(self)
+            token = self._input.LA(1)
+            if token in [TacticNotationsParser.PIPE]:
+                self.enterOuterAlt(localctx, 1)
+                self.state = 43
+                self.pipe()
+                pass
+            elif token in [TacticNotationsParser.LALT, TacticNotationsParser.LGROUP, TacticNotationsParser.LBRACE, TacticNotationsParser.ESCAPED, TacticNotationsParser.ATOM, TacticNotationsParser.ID]:
+                self.enterOuterAlt(localctx, 2)
+                self.state = 44
+                self.nopipeblock()
+                pass
+            else:
+                raise NoViableAltException(self)
+
+        except RecognitionException as re:
+            localctx.exception = re
+            self._errHandler.reportError(self, re)
+            self._errHandler.recover(self, re)
+        finally:
+            self.exitRule()
+        return localctx
+
+    class NopipeblockContext(ParserRuleContext):
+
+        def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1):
+            super().__init__(parent, invokingState)
+            self.parser = parser
+
         def atomic(self):
             return self.getTypedRuleContext(TacticNotationsParser.AtomicContext,0)
 
 
-        def meta(self):
-            return self.getTypedRuleContext(TacticNotationsParser.MetaContext,0)
+        def escaped(self):
+            return self.getTypedRuleContext(TacticNotationsParser.EscapedContext,0)
 
 
         def hole(self):
             return self.getTypedRuleContext(TacticNotationsParser.HoleContext,0)
 
 
+        def alternative(self):
+            return self.getTypedRuleContext(TacticNotationsParser.AlternativeContext,0)
+
+
         def repeat(self):
             return self.getTypedRuleContext(TacticNotationsParser.RepeatContext,0)
 
@@ -219,48 +304,53 @@ class TacticNotationsParser ( Parser ):
 
 
         def getRuleIndex(self):
-            return TacticNotationsParser.RULE_block
+            return TacticNotationsParser.RULE_nopipeblock
 
         def accept(self, visitor:ParseTreeVisitor):
-            if hasattr( visitor, "visitBlock" ):
-                return visitor.visitBlock(self)
+            if hasattr( visitor, "visitNopipeblock" ):
+                return visitor.visitNopipeblock(self)
             else:
                 return visitor.visitChildren(self)
 
 
 
 
-    def block(self):
+    def nopipeblock(self):
 
-        localctx = TacticNotationsParser.BlockContext(self, self._ctx, self.state)
-        self.enterRule(localctx, 4, self.RULE_block)
+        localctx = TacticNotationsParser.NopipeblockContext(self, self._ctx, self.state)
+        self.enterRule(localctx, 6, self.RULE_nopipeblock)
         try:
-            self.state = 36
+            self.state = 53
             self._errHandler.sync(self)
             token = self._input.LA(1)
             if token in [TacticNotationsParser.ATOM]:
                 self.enterOuterAlt(localctx, 1)
-                self.state = 31
+                self.state = 47
                 self.atomic()
                 pass
-            elif token in [TacticNotationsParser.METACHAR]:
+            elif token in [TacticNotationsParser.ESCAPED]:
                 self.enterOuterAlt(localctx, 2)
-                self.state = 32
-                self.meta()
+                self.state = 48
+                self.escaped()
                 pass
             elif token in [TacticNotationsParser.ID]:
                 self.enterOuterAlt(localctx, 3)
-                self.state = 33
+                self.state = 49
                 self.hole()
                 pass
-            elif token in [TacticNotationsParser.LGROUP]:
+            elif token in [TacticNotationsParser.LALT]:
                 self.enterOuterAlt(localctx, 4)
-                self.state = 34
+                self.state = 50
+                self.alternative()
+                pass
+            elif token in [TacticNotationsParser.LGROUP]:
+                self.enterOuterAlt(localctx, 5)
+                self.state = 51
                 self.repeat()
                 pass
             elif token in [TacticNotationsParser.LBRACE]:
-                self.enterOuterAlt(localctx, 5)
-                self.state = 35
+                self.enterOuterAlt(localctx, 6)
+                self.state = 52
                 self.curlies()
                 pass
             else:
@@ -274,6 +364,232 @@ class TacticNotationsParser ( Parser ):
             self.exitRule()
         return localctx
 
+    class AlternativeContext(ParserRuleContext):
+
+        def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1):
+            super().__init__(parent, invokingState)
+            self.parser = parser
+
+        def LALT(self):
+            return self.getToken(TacticNotationsParser.LALT, 0)
+
+        def altblocks(self):
+            return self.getTypedRuleContext(TacticNotationsParser.AltblocksContext,0)
+
+
+        def RBRACE(self):
+            return self.getToken(TacticNotationsParser.RBRACE, 0)
+
+        def WHITESPACE(self, i:int=None):
+            if i is None:
+                return self.getTokens(TacticNotationsParser.WHITESPACE)
+            else:
+                return self.getToken(TacticNotationsParser.WHITESPACE, i)
+
+        def getRuleIndex(self):
+            return TacticNotationsParser.RULE_alternative
+
+        def accept(self, visitor:ParseTreeVisitor):
+            if hasattr( visitor, "visitAlternative" ):
+                return visitor.visitAlternative(self)
+            else:
+                return visitor.visitChildren(self)
+
+
+
+
+    def alternative(self):
+
+        localctx = TacticNotationsParser.AlternativeContext(self, self._ctx, self.state)
+        self.enterRule(localctx, 8, self.RULE_alternative)
+        self._la = 0 # Token type
+        try:
+            self.enterOuterAlt(localctx, 1)
+            self.state = 55
+            self.match(TacticNotationsParser.LALT)
+            self.state = 57
+            self._errHandler.sync(self)
+            _la = self._input.LA(1)
+            if _la==TacticNotationsParser.WHITESPACE:
+                self.state = 56
+                self.match(TacticNotationsParser.WHITESPACE)
+
+
+            self.state = 59
+            self.altblocks()
+            self.state = 61
+            self._errHandler.sync(self)
+            _la = self._input.LA(1)
+            if _la==TacticNotationsParser.WHITESPACE:
+                self.state = 60
+                self.match(TacticNotationsParser.WHITESPACE)
+
+
+            self.state = 63
+            self.match(TacticNotationsParser.RBRACE)
+        except RecognitionException as re:
+            localctx.exception = re
+            self._errHandler.reportError(self, re)
+            self._errHandler.recover(self, re)
+        finally:
+            self.exitRule()
+        return localctx
+
+    class AltblocksContext(ParserRuleContext):
+
+        def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1):
+            super().__init__(parent, invokingState)
+            self.parser = parser
+
+        def altblock(self, i:int=None):
+            if i is None:
+                return self.getTypedRuleContexts(TacticNotationsParser.AltblockContext)
+            else:
+                return self.getTypedRuleContext(TacticNotationsParser.AltblockContext,i)
+
+
+        def altsep(self, i:int=None):
+            if i is None:
+                return self.getTypedRuleContexts(TacticNotationsParser.AltsepContext)
+            else:
+                return self.getTypedRuleContext(TacticNotationsParser.AltsepContext,i)
+
+
+        def WHITESPACE(self, i:int=None):
+            if i is None:
+                return self.getTokens(TacticNotationsParser.WHITESPACE)
+            else:
+                return self.getToken(TacticNotationsParser.WHITESPACE, i)
+
+        def getRuleIndex(self):
+            return TacticNotationsParser.RULE_altblocks
+
+        def accept(self, visitor:ParseTreeVisitor):
+            if hasattr( visitor, "visitAltblocks" ):
+                return visitor.visitAltblocks(self)
+            else:
+                return visitor.visitChildren(self)
+
+
+
+
+    def altblocks(self):
+
+        localctx = TacticNotationsParser.AltblocksContext(self, self._ctx, self.state)
+        self.enterRule(localctx, 10, self.RULE_altblocks)
+        self._la = 0 # Token type
+        try:
+            self.enterOuterAlt(localctx, 1)
+            self.state = 65
+            self.altblock()
+            self.state = 75
+            self._errHandler.sync(self)
+            _alt = 1
+            while _alt!=2 and _alt!=ATN.INVALID_ALT_NUMBER:
+                if _alt == 1:
+                    self.state = 67
+                    self._errHandler.sync(self)
+                    _la = self._input.LA(1)
+                    if _la==TacticNotationsParser.WHITESPACE:
+                        self.state = 66
+                        self.match(TacticNotationsParser.WHITESPACE)
+
+
+                    self.state = 69
+                    self.altsep()
+                    self.state = 71
+                    self._errHandler.sync(self)
+                    _la = self._input.LA(1)
+                    if _la==TacticNotationsParser.WHITESPACE:
+                        self.state = 70
+                        self.match(TacticNotationsParser.WHITESPACE)
+
+
+                    self.state = 73
+                    self.altblock()
+
+                else:
+                    raise NoViableAltException(self)
+                self.state = 77
+                self._errHandler.sync(self)
+                _alt = self._interp.adaptivePredict(self._input,8,self._ctx)
+
+        except RecognitionException as re:
+            localctx.exception = re
+            self._errHandler.reportError(self, re)
+            self._errHandler.recover(self, re)
+        finally:
+            self.exitRule()
+        return localctx
+
+    class AltblockContext(ParserRuleContext):
+
+        def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1):
+            super().__init__(parent, invokingState)
+            self.parser = parser
+
+        def nopipeblock(self, i:int=None):
+            if i is None:
+                return self.getTypedRuleContexts(TacticNotationsParser.NopipeblockContext)
+            else:
+                return self.getTypedRuleContext(TacticNotationsParser.NopipeblockContext,i)
+
+
+        def whitespace(self, i:int=None):
+            if i is None:
+                return self.getTypedRuleContexts(TacticNotationsParser.WhitespaceContext)
+            else:
+                return self.getTypedRuleContext(TacticNotationsParser.WhitespaceContext,i)
+
+
+        def getRuleIndex(self):
+            return TacticNotationsParser.RULE_altblock
+
+        def accept(self, visitor:ParseTreeVisitor):
+            if hasattr( visitor, "visitAltblock" ):
+                return visitor.visitAltblock(self)
+            else:
+                return visitor.visitChildren(self)
+
+
+
+
+    def altblock(self):
+
+        localctx = TacticNotationsParser.AltblockContext(self, self._ctx, self.state)
+        self.enterRule(localctx, 12, self.RULE_altblock)
+        self._la = 0 # Token type
+        try:
+            self.enterOuterAlt(localctx, 1)
+            self.state = 79
+            self.nopipeblock()
+            self.state = 86
+            self._errHandler.sync(self)
+            _alt = self._interp.adaptivePredict(self._input,10,self._ctx)
+            while _alt!=2 and _alt!=ATN.INVALID_ALT_NUMBER:
+                if _alt==1:
+                    self.state = 81
+                    self._errHandler.sync(self)
+                    _la = self._input.LA(1)
+                    if _la==TacticNotationsParser.WHITESPACE:
+                        self.state = 80
+                        self.whitespace()
+
+
+                    self.state = 83
+                    self.nopipeblock()
+                self.state = 88
+                self._errHandler.sync(self)
+                _alt = self._interp.adaptivePredict(self._input,10,self._ctx)
+
+        except RecognitionException as re:
+            localctx.exception = re
+            self._errHandler.reportError(self, re)
+            self._errHandler.recover(self, re)
+        finally:
+            self.exitRule()
+        return localctx
+
     class RepeatContext(ParserRuleContext):
 
         def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1):
@@ -299,6 +615,9 @@ class TacticNotationsParser ( Parser ):
         def ATOM(self):
             return self.getToken(TacticNotationsParser.ATOM, 0)
 
+        def PIPE(self):
+            return self.getToken(TacticNotationsParser.PIPE, 0)
+
         def getRuleIndex(self):
             return TacticNotationsParser.RULE_repeat
 
@@ -314,33 +633,38 @@ class TacticNotationsParser ( Parser ):
     def repeat(self):
 
         localctx = TacticNotationsParser.RepeatContext(self, self._ctx, self.state)
-        self.enterRule(localctx, 6, self.RULE_repeat)
+        self.enterRule(localctx, 14, self.RULE_repeat)
         self._la = 0 # Token type
         try:
             self.enterOuterAlt(localctx, 1)
-            self.state = 38
+            self.state = 89
             self.match(TacticNotationsParser.LGROUP)
-            self.state = 40
+            self.state = 91
             self._errHandler.sync(self)
             _la = self._input.LA(1)
-            if _la==TacticNotationsParser.ATOM:
-                self.state = 39
-                self.match(TacticNotationsParser.ATOM)
+            if _la==TacticNotationsParser.PIPE or _la==TacticNotationsParser.ATOM:
+                self.state = 90
+                _la = self._input.LA(1)
+                if not(_la==TacticNotationsParser.PIPE or _la==TacticNotationsParser.ATOM):
+                    self._errHandler.recoverInline(self)
+                else:
+                    self._errHandler.reportMatch(self)
+                    self.consume()
 
 
-            self.state = 42
+            self.state = 93
             self.match(TacticNotationsParser.WHITESPACE)
-            self.state = 43
+            self.state = 94
             self.blocks()
-            self.state = 45
+            self.state = 96
             self._errHandler.sync(self)
             _la = self._input.LA(1)
             if _la==TacticNotationsParser.WHITESPACE:
-                self.state = 44
+                self.state = 95
                 self.match(TacticNotationsParser.WHITESPACE)
 
 
-            self.state = 47
+            self.state = 98
             self.match(TacticNotationsParser.RBRACE)
         except RecognitionException as re:
             localctx.exception = re
@@ -388,31 +712,31 @@ class TacticNotationsParser ( Parser ):
     def curlies(self):
 
         localctx = TacticNotationsParser.CurliesContext(self, self._ctx, self.state)
-        self.enterRule(localctx, 8, self.RULE_curlies)
+        self.enterRule(localctx, 16, self.RULE_curlies)
         self._la = 0 # Token type
         try:
             self.enterOuterAlt(localctx, 1)
-            self.state = 49
+            self.state = 100
             self.match(TacticNotationsParser.LBRACE)
-            self.state = 51
+            self.state = 102
             self._errHandler.sync(self)
             _la = self._input.LA(1)
             if _la==TacticNotationsParser.WHITESPACE:
-                self.state = 50
+                self.state = 101
                 self.whitespace()
 
 
-            self.state = 53
+            self.state = 104
             self.blocks()
-            self.state = 55
+            self.state = 106
             self._errHandler.sync(self)
             _la = self._input.LA(1)
             if _la==TacticNotationsParser.WHITESPACE:
-                self.state = 54
+                self.state = 105
                 self.whitespace()
 
 
-            self.state = 57
+            self.state = 108
             self.match(TacticNotationsParser.RBRACE)
         except RecognitionException as re:
             localctx.exception = re
@@ -422,6 +746,80 @@ class TacticNotationsParser ( Parser ):
             self.exitRule()
         return localctx
 
+    class PipeContext(ParserRuleContext):
+
+        def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1):
+            super().__init__(parent, invokingState)
+            self.parser = parser
+
+        def PIPE(self):
+            return self.getToken(TacticNotationsParser.PIPE, 0)
+
+        def getRuleIndex(self):
+            return TacticNotationsParser.RULE_pipe
+
+        def accept(self, visitor:ParseTreeVisitor):
+            if hasattr( visitor, "visitPipe" ):
+                return visitor.visitPipe(self)
+            else:
+                return visitor.visitChildren(self)
+
+
+
+
+    def pipe(self):
+
+        localctx = TacticNotationsParser.PipeContext(self, self._ctx, self.state)
+        self.enterRule(localctx, 18, self.RULE_pipe)
+        try:
+            self.enterOuterAlt(localctx, 1)
+            self.state = 110
+            self.match(TacticNotationsParser.PIPE)
+        except RecognitionException as re:
+            localctx.exception = re
+            self._errHandler.reportError(self, re)
+            self._errHandler.recover(self, re)
+        finally:
+            self.exitRule()
+        return localctx
+
+    class AltsepContext(ParserRuleContext):
+
+        def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1):
+            super().__init__(parent, invokingState)
+            self.parser = parser
+
+        def PIPE(self):
+            return self.getToken(TacticNotationsParser.PIPE, 0)
+
+        def getRuleIndex(self):
+            return TacticNotationsParser.RULE_altsep
+
+        def accept(self, visitor:ParseTreeVisitor):
+            if hasattr( visitor, "visitAltsep" ):
+                return visitor.visitAltsep(self)
+            else:
+                return visitor.visitChildren(self)
+
+
+
+
+    def altsep(self):
+
+        localctx = TacticNotationsParser.AltsepContext(self, self._ctx, self.state)
+        self.enterRule(localctx, 20, self.RULE_altsep)
+        try:
+            self.enterOuterAlt(localctx, 1)
+            self.state = 112
+            self.match(TacticNotationsParser.PIPE)
+        except RecognitionException as re:
+            localctx.exception = re
+            self._errHandler.reportError(self, re)
+            self._errHandler.recover(self, re)
+        finally:
+            self.exitRule()
+        return localctx
+
     class WhitespaceContext(ParserRuleContext):
 
         def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1):
@@ -446,10 +844,10 @@ class TacticNotationsParser ( Parser ):
     def whitespace(self):
 
         localctx = TacticNotationsParser.WhitespaceContext(self, self._ctx, self.state)
-        self.enterRule(localctx, 10, self.RULE_whitespace)
+        self.enterRule(localctx, 22, self.RULE_whitespace)
         try:
             self.enterOuterAlt(localctx, 1)
-            self.state = 59
+            self.state = 114
             self.match(TacticNotationsParser.WHITESPACE)
         except RecognitionException as re:
             localctx.exception = re
@@ -459,35 +857,35 @@ class TacticNotationsParser ( Parser ):
             self.exitRule()
         return localctx
 
-    class MetaContext(ParserRuleContext):
+    class EscapedContext(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 ESCAPED(self):
+            return self.getToken(TacticNotationsParser.ESCAPED, 0)
 
         def getRuleIndex(self):
-            return TacticNotationsParser.RULE_meta
+            return TacticNotationsParser.RULE_escaped
 
         def accept(self, visitor:ParseTreeVisitor):
-            if hasattr( visitor, "visitMeta" ):
-                return visitor.visitMeta(self)
+            if hasattr( visitor, "visitEscaped" ):
+                return visitor.visitEscaped(self)
             else:
                 return visitor.visitChildren(self)
 
 
 
 
-    def meta(self):
+    def escaped(self):
 
-        localctx = TacticNotationsParser.MetaContext(self, self._ctx, self.state)
-        self.enterRule(localctx, 12, self.RULE_meta)
+        localctx = TacticNotationsParser.EscapedContext(self, self._ctx, self.state)
+        self.enterRule(localctx, 24, self.RULE_escaped)
         try:
             self.enterOuterAlt(localctx, 1)
-            self.state = 61
-            self.match(TacticNotationsParser.METACHAR)
+            self.state = 116
+            self.match(TacticNotationsParser.ESCAPED)
         except RecognitionException as re:
             localctx.exception = re
             self._errHandler.reportError(self, re)
@@ -523,17 +921,17 @@ class TacticNotationsParser ( Parser ):
     def atomic(self):
 
         localctx = TacticNotationsParser.AtomicContext(self, self._ctx, self.state)
-        self.enterRule(localctx, 14, self.RULE_atomic)
+        self.enterRule(localctx, 26, self.RULE_atomic)
         self._la = 0 # Token type
         try:
             self.enterOuterAlt(localctx, 1)
-            self.state = 63
+            self.state = 118
             self.match(TacticNotationsParser.ATOM)
-            self.state = 65
+            self.state = 120
             self._errHandler.sync(self)
             _la = self._input.LA(1)
             if _la==TacticNotationsParser.SUB:
-                self.state = 64
+                self.state = 119
                 self.match(TacticNotationsParser.SUB)
 
 
@@ -572,17 +970,17 @@ class TacticNotationsParser ( Parser ):
     def hole(self):
 
         localctx = TacticNotationsParser.HoleContext(self, self._ctx, self.state)
-        self.enterRule(localctx, 16, self.RULE_hole)
+        self.enterRule(localctx, 28, self.RULE_hole)
         self._la = 0 # Token type
         try:
             self.enterOuterAlt(localctx, 1)
-            self.state = 67
+            self.state = 122
             self.match(TacticNotationsParser.ID)
-            self.state = 69
+            self.state = 124
             self._errHandler.sync(self)
             _la = self._input.LA(1)
             if _la==TacticNotationsParser.SUB:
-                self.state = 68
+                self.state = 123
                 self.match(TacticNotationsParser.SUB)
 
 
diff --git a/doc/tools/coqrst/notations/TacticNotationsVisitor.py b/doc/tools/coqrst/notations/TacticNotationsVisitor.py
index c0bcc4af37..aba696c89f 100644
--- a/doc/tools/coqrst/notations/TacticNotationsVisitor.py
+++ b/doc/tools/coqrst/notations/TacticNotationsVisitor.py
@@ -1,4 +1,4 @@
-# Generated from TacticNotations.g by ANTLR 4.7
+# Generated from TacticNotations.g by ANTLR 4.7.2
 from antlr4 import *
 if __name__ is not None and "." in __name__:
     from .TacticNotationsParser import TacticNotationsParser
@@ -24,6 +24,26 @@ class TacticNotationsVisitor(ParseTreeVisitor):
         return self.visitChildren(ctx)
 
 
+    # Visit a parse tree produced by TacticNotationsParser#nopipeblock.
+    def visitNopipeblock(self, ctx:TacticNotationsParser.NopipeblockContext):
+        return self.visitChildren(ctx)
+
+
+    # Visit a parse tree produced by TacticNotationsParser#alternative.
+    def visitAlternative(self, ctx:TacticNotationsParser.AlternativeContext):
+        return self.visitChildren(ctx)
+
+
+    # Visit a parse tree produced by TacticNotationsParser#altblocks.
+    def visitAltblocks(self, ctx:TacticNotationsParser.AltblocksContext):
+        return self.visitChildren(ctx)
+
+
+    # Visit a parse tree produced by TacticNotationsParser#altblock.
+    def visitAltblock(self, ctx:TacticNotationsParser.AltblockContext):
+        return self.visitChildren(ctx)
+
+
     # Visit a parse tree produced by TacticNotationsParser#repeat.
     def visitRepeat(self, ctx:TacticNotationsParser.RepeatContext):
         return self.visitChildren(ctx)
@@ -34,13 +54,23 @@ class TacticNotationsVisitor(ParseTreeVisitor):
         return self.visitChildren(ctx)
 
 
+    # Visit a parse tree produced by TacticNotationsParser#pipe.
+    def visitPipe(self, ctx:TacticNotationsParser.PipeContext):
+        return self.visitChildren(ctx)
+
+
+    # Visit a parse tree produced by TacticNotationsParser#altsep.
+    def visitAltsep(self, ctx:TacticNotationsParser.AltsepContext):
+        return self.visitChildren(ctx)
+
+
     # Visit a parse tree produced by TacticNotationsParser#whitespace.
     def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext):
         return self.visitChildren(ctx)
 
 
-    # Visit a parse tree produced by TacticNotationsParser#meta.
-    def visitMeta(self, ctx:TacticNotationsParser.MetaContext):
+    # Visit a parse tree produced by TacticNotationsParser#escaped.
+    def visitEscaped(self, ctx:TacticNotationsParser.EscapedContext):
         return self.visitChildren(ctx)
 
 
diff --git a/doc/tools/coqrst/notations/html.py b/doc/tools/coqrst/notations/html.py
index 87a41cf9f3..d2b5d86b37 100644
--- a/doc/tools/coqrst/notations/html.py
+++ b/doc/tools/coqrst/notations/html.py
@@ -13,12 +13,24 @@ Uses the dominate package.
 """
 
 from dominate import tags
+from dominate.utils import text
 
 from .parsing import parse
 from .TacticNotationsParser import TacticNotationsParser
 from .TacticNotationsVisitor import TacticNotationsVisitor
 
 class TacticNotationsToHTMLVisitor(TacticNotationsVisitor):
+    def visitAlternative(self, ctx:TacticNotationsParser.AlternativeContext):
+        with tags.span(_class='alternative'):
+            self.visitChildren(ctx)
+
+    def visitAltblock(self, ctx:TacticNotationsParser.AltblockContext):
+        with tags.span(_class='alternative-block'):
+            self.visitChildren(ctx)
+
+    def visitAltsep(self, ctx:TacticNotationsParser.AltsepContext):
+        tags.span('\u200b', _class="alternative-separator")
+
     def visitRepeat(self, ctx:TacticNotationsParser.RepeatContext):
         with tags.span(_class="repeat-wrapper"):
             with tags.span(_class="repeat"):
@@ -39,21 +51,20 @@ class TacticNotationsToHTMLVisitor(TacticNotationsVisitor):
     def visitAtomic(self, ctx:TacticNotationsParser.AtomicContext):
         tags.span(ctx.ATOM().getText())
 
+    def visitPipe(self, ctx:TacticNotationsParser.PipeContext):
+        text("|")
+
     def visitHole(self, ctx:TacticNotationsParser.HoleContext):
         tags.span(ctx.ID().getText()[1:], _class="hole")
         sub = ctx.SUB()
         if sub:
             tags.sub(sub.getText()[1:])
 
-    def visitMeta(self, ctx:TacticNotationsParser.MetaContext):
-        txt = ctx.METACHAR().getText()[1:]
-        if (txt == "{") or (txt == "}"):
-            tags.span(txt)
-        else:
-            tags.span(txt, _class="meta")
+    def visitEscaped(self, ctx:TacticNotationsParser.EscapedContext):
+        tags.span(ctx.ESCAPED().getText()[1:])
 
     def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext):
-        tags.span(" ")          # TODO: no need for a <span> here
+        text(" ")
 
 def htmlize(notation):
     """Translate notation to a dominate HTML tree"""
diff --git a/doc/tools/coqrst/notations/plain.py b/doc/tools/coqrst/notations/plain.py
index f6e82fc68e..2180c8e6a5 100644
--- a/doc/tools/coqrst/notations/plain.py
+++ b/doc/tools/coqrst/notations/plain.py
@@ -22,8 +22,16 @@ class TacticNotationsToDotsVisitor(TacticNotationsVisitor):
     def __init__(self):
         self.buffer = StringIO()
 
+    def visitAlternative(self, ctx:TacticNotationsParser.AlternativeContext):
+        self.buffer.write("[")
+        self.visitChildren(ctx)
+        self.buffer.write("]")
+
+    def visitAltsep(self, ctx:TacticNotationsParser.AltsepContext):
+        self.buffer.write("|")
+
     def visitRepeat(self, ctx:TacticNotationsParser.RepeatContext):
-        separator = ctx.ATOM()
+        separator = ctx.ATOM() or ctx.PIPE()
         self.visitChildren(ctx)
         if ctx.LGROUP().getText()[1] == "+":
             spacer = (separator.getText() + " " if separator else "")
@@ -38,11 +46,14 @@ class TacticNotationsToDotsVisitor(TacticNotationsVisitor):
     def visitAtomic(self, ctx:TacticNotationsParser.AtomicContext):
         self.buffer.write(ctx.ATOM().getText())
 
+    def visitPipe(self, ctx:TacticNotationsParser.PipeContext):
+        self.buffer.write("|")
+
     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 visitEscaped(self, ctx:TacticNotationsParser.EscapedContext):
+        self.buffer.write(ctx.ESCAPED().getText()[1:])
 
     def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext):
         self.buffer.write(" ")
diff --git a/doc/tools/coqrst/notations/sphinx.py b/doc/tools/coqrst/notations/sphinx.py
index e05b834184..4ed09e04a9 100644
--- a/doc/tools/coqrst/notations/sphinx.py
+++ b/doc/tools/coqrst/notations/sphinx.py
@@ -20,8 +20,6 @@ from .TacticNotationsVisitor import TacticNotationsVisitor
 from docutils import nodes
 from sphinx import addnodes
 
-import sys
-
 class TacticNotationsToSphinxVisitor(TacticNotationsVisitor):
     def defaultResult(self):
         return []
@@ -31,16 +29,36 @@ class TacticNotationsToSphinxVisitor(TacticNotationsVisitor):
             aggregate.extend(nextResult)
         return aggregate
 
+    def visitAlternative(self, ctx:TacticNotationsParser.AlternativeContext):
+        return [nodes.inline('', '', *self.visitChildren(ctx), classes=['alternative'])]
+
+    def visitAltblock(self, ctx:TacticNotationsParser.AltblockContext):
+        return [nodes.inline('', '', *self.visitChildren(ctx), classes=['alternative-block'])]
+
+    def visitAltsep(self, ctx:TacticNotationsParser.AltsepContext):
+        return [nodes.inline('|', '\u200b', classes=['alternative-separator'])]
+
+    @staticmethod
+    def is_alternative(node):
+        return isinstance(node, nodes.inline) and node['classes'] == ['alternative']
+
     def visitRepeat(self, ctx:TacticNotationsParser.RepeatContext):
         # Uses inline nodes instead of subscript and superscript to ensure that
         # we get the right customization hooks at the LaTeX level
         wrapper = nodes.inline('', '', classes=['repeat-wrapper'])
-        wrapper += nodes.inline('', '', *self.visitChildren(ctx), classes=["repeat"])
+
+        children = self.visitChildren(ctx)
+        if len(children) == 1 and self.is_alternative(children[0]):
+            # Use a custom style if an alternative is nested in a repeat.
+            # (We could detect this in CSS, but it's much harder in LaTeX.)
+
+            children[0]['classes'] = ['repeated-alternative']
+        wrapper += nodes.inline('', '', *children, classes=["repeat"])
 
         repeat_marker = ctx.LGROUP().getText()[1]
         wrapper += nodes.inline(repeat_marker, repeat_marker, classes=['notation-sup'])
 
-        separator = ctx.ATOM()
+        separator = ctx.ATOM() or ctx.PIPE()
         if separator:
             sep = separator.getText()
             wrapper += nodes.inline(sep, sep, classes=['notation-sub'])
@@ -65,6 +83,9 @@ class TacticNotationsToSphinxVisitor(TacticNotationsVisitor):
 
         return [node]
 
+    def visitPipe(self, ctx:TacticNotationsParser.PipeContext):
+        return [nodes.Text("|")]
+
     def visitHole(self, ctx:TacticNotationsParser.HoleContext):
         hole = ctx.ID().getText()
         token_name = hole[1:]
@@ -75,23 +96,18 @@ class TacticNotationsToSphinxVisitor(TacticNotationsVisitor):
             sub_index = sub.getText()[2:]
             node += nodes.subscript(sub_index, sub_index)
 
-        return [addnodes.pending_xref(token_name, node, reftype='token', refdomain='std', reftarget=token_name)]
+        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
-        if (metachar == "{") or (metachar == "}"):
-            classes=[]
-        else:
-            classes=["meta"]
-        return [nodes.inline(metachar, token_name, classes=classes)]
+    def visitEscaped(self, ctx:TacticNotationsParser.EscapedContext):
+        escaped = ctx.ESCAPED().getText()
+        return [nodes.inline(escaped, escaped[1:])]
 
     def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext):
         return [nodes.Text(" ")]
 
 def sphinxify(notation):
-    """Translate notation into a Sphinx document tree"""
+    """Translate a notation into a Sphinx document tree."""
     vs = TacticNotationsToSphinxVisitor()
     return vs.visit(parse(notation))