Merge PR #10143: Add dedicated syntax for alternatives (abc | def) in manual notations

Reviewed-by: Zimmi48
Ack-by: jfehrle

26 files changed, 869 insertions, 277 deletions

diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index 881f7a310d..b20669c7f1 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -60,8 +60,11 @@ The signatures of most objects can be written using a succinct DSL for Coq notat
 ``{*, …}``, ``{+, …}``
   an optional or mandatory repeatable block, with repetitions separated by commas
 
-``%|``, ``%{``, …
-  an escaped character (rendered without the leading ``%``)
+``{| … | … | … }``
+  an alternative, indicating than one of multiple constructs can be used
+
+``%{``, ``%}``, ``%|``
+  an escaped character (rendered without the leading ``%``).  In most cases, escaping is not necessary.  In particular, the following expressions are all parsed as plain text, and do not need escaping: ``{ xyz }``, ``x |- y``.  But the following escapes *are* needed: ``{| a b %| c | d }``, ``all: %{``.  (We use ``%`` instead of the usual ``\`` because you'd have to type ``\`` twice in your reStructuredText file.)
 
 ..
    FIXME document the new subscript support
@@ -148,7 +151,7 @@ Here is the list of all objects of the Coq domain (The symbol :black_nib: indica
     Example::
 
         .. prodn:: term += let: @pattern := @term in @term
-        .. prodn:: occ_switch ::= { {? + %| - } {* @num } }
+        .. prodn:: occ_switch ::= { {? {| + | - } } {* @num } }
 
 ``.. table::`` :black_nib: A Coq table, i.e. a setting that is a set of values.
     Example::
diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst
index 78803a927f..2093765608 100644
--- a/doc/sphinx/README.template.rst
+++ b/doc/sphinx/README.template.rst
@@ -60,8 +60,11 @@ The signatures of most objects can be written using a succinct DSL for Coq notat
 ``{*, …}``, ``{+, …}``
   an optional or mandatory repeatable block, with repetitions separated by commas
 
-``%|``, ``%{``, …
-  an escaped character (rendered without the leading ``%``)
+``{| … | … | … }``
+  an alternative, indicating than one of multiple constructs can be used
+
+``%{``, ``%}``, ``%|``
+  an escaped character (rendered without the leading ``%``).  In most cases, escaping is not necessary.  In particular, the following expressions are all parsed as plain text, and do not need escaping: ``{ xyz }``, ``x |- y``.  But the following escapes *are* needed: ``{| a b %| c | d }``, ``all: %{``.  (We use ``%`` instead of the usual ``\`` because you'd have to type ``\`` twice in your reStructuredText file.)
 
 ..
    FIXME document the new subscript support
diff --git a/doc/sphinx/_static/coqnotations.sty b/doc/sphinx/_static/coqnotations.sty
index 75eac1f724..3548b8754c 100644
--- a/doc/sphinx/_static/coqnotations.sty
+++ b/doc/sphinx/_static/coqnotations.sty
@@ -18,6 +18,9 @@
 \newlength{\nscriptsize}
 \setlength{\nscriptsize}{0.8em}
 
+\newlength{\nboxsep}
+\setlength{\nboxsep}{2pt}
+
 \newcommand*{\scriptsmallsquarebox}[1]{%
   % Force width
   \makebox[\nscriptsize]{%
@@ -31,7 +34,8 @@
 \newcommand*{\nsup}[1]{^{\nscript{0.15}{#1}}}
 \newcommand*{\nsub}[1]{_{\nscript{0.35}{#1}}}
 \newcommand*{\nnotation}[1]{#1}
-\newcommand*{\nrepeat}[1]{\text{\adjustbox{cfbox=nbordercolor 0.5pt 2pt,bgcolor=nbgcolor}{#1\hspace{.5\nscriptsize}}}}
+\newcommand*{\nbox}[1]{\adjustbox{cfbox=nbordercolor 0.5pt \nboxsep,bgcolor=nbgcolor}{#1}}
+\newcommand*{\nrepeat}[1]{\text{\nbox{#1\hspace{.5\nscriptsize}}}}
 \newcommand*{\nwrapper}[1]{\ensuremath{\displaystyle#1}} % https://tex.stackexchange.com/questions/310877/
 \newcommand*{\nhole}[1]{\textit{\color{nholecolor}#1}}
 
@@ -42,9 +46,32 @@
 }
 % </magic>
 
+% https://tex.stackexchange.com/questions/490262/
+\def\naltsep{}
+\newsavebox{\nsavedalt}
+\newlength{\naltvruleht}
+\newlength{\naltvruledp}
+\def\naltvrule{\smash{\vrule height\naltvruleht depth\naltvruledp}}
+\newcommand{\nalternative}[2]{%
+  % First measure the contents of the box without the bar
+  \bgroup%
+  \def\naltsep{}%
+  \savebox{\nsavedalt}{#1}%
+  \setlength{\naltvruleht}{\ht\nsavedalt}%
+  \setlength{\naltvruledp}{\dp\nsavedalt}%
+  \addtolength{\naltvruleht}{#2}%
+  \addtolength{\naltvruledp}{#2}%
+  % Then redraw it with the bar
+  \def\naltsep{\naltvrule}%
+  #1\egroup}
+
 \newcssclass{notation-sup}{\nsup{#1}}
 \newcssclass{notation-sub}{\nsub{#1}}
 \newcssclass{notation}{\nnotation{#1}}
 \newcssclass{repeat}{\nrepeat{#1}}
 \newcssclass{repeat-wrapper}{\nwrapper{#1}}
 \newcssclass{hole}{\nhole{#1}}
+\newcssclass{alternative}{\nalternative{\nbox{#1}}{0pt}}
+\newcssclass{alternative-block}{#1}
+\newcssclass{repeated-alternative}{\nalternative{#1}{\nboxsep}}
+\newcssclass{alternative-separator}{\quad\naltsep{}\quad}
diff --git a/doc/sphinx/_static/notations.css b/doc/sphinx/_static/notations.css
index dcb47d1786..8322ab0137 100644
--- a/doc/sphinx/_static/notations.css
+++ b/doc/sphinx/_static/notations.css
@@ -45,15 +45,46 @@
     width: 2.2em;
 }
 
-.notation .repeat {
+.notation .repeat, .notation .alternative {
     background: #EAEAEA;
     border: 1px solid #AAA;
     display: inline-block;
-    padding-right: 0.6em; /* Space for the left half of the sub- and sup-scripts */
-    padding-left: 0.2em;
+    padding: 0 0.2em 0 0.3em;
     margin: 0.25em 0;
 }
 
+.notation .repeated-alternative {
+    display: inline-table;
+}
+
+.notation .alternative {
+    display: inline-table;
+    padding: 0 0.2em;
+}
+
+.notation .alternative-block {
+    display: table-cell;
+    padding: 0 0.5em;
+}
+
+.notation .alternative-separator {
+    border-left: 1px solid black; /* Display a thin bar */
+    display: table-cell;
+    width: 0;
+}
+
+.alternative-block:first-child {
+  padding-left: 0;
+}
+
+.alternative-block:last-child {
+  padding-right: 0;
+}
+
+.notation .repeat {
+    padding-right: 0.6em; /* Space for the left half of the sub- and sup-scripts */
+}
+
 .notation .repeat-wrapper {
     display: inline-block;
     position: relative;
diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst
index e93b01f14d..8a895eb515 100644
--- a/doc/sphinx/addendum/extraction.rst
+++ b/doc/sphinx/addendum/extraction.rst
@@ -99,7 +99,7 @@ Extraction Options
 Setting the target language
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. cmd:: Extraction Language ( OCaml | Haskell | Scheme )
+.. cmd:: Extraction Language {| OCaml | Haskell | Scheme }
    :name: Extraction Language
 
    The ability to fix target language is the first and more important
diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst
index b474c51f17..4d9e8d8b3a 100644
--- a/doc/sphinx/addendum/generalized-rewriting.rst
+++ b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -809,7 +809,7 @@ Usage
 ~~~~~
 
 
-.. tacn:: rewrite_strat @s [in @ident]
+.. tacn:: rewrite_strat @s {? in @ident }
    :name: rewrite_strat
 
    Rewrite using the strategy s in hypothesis ident or the conclusion.
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index b410833d25..22ddcae584 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -283,7 +283,7 @@ optional identifier is used when multiple functions have unsolved
 obligations (e.g. when defining mutually recursive blocks). The
 optional tactic is replaced by the default one if not specified.
 
-.. cmd:: {? Local|Global} Obligation Tactic := @tactic
+.. cmd:: {? {| Local | Global } } Obligation Tactic := @tactic
    :name: Obligation Tactic
 
    Sets the default obligation solving tactic applied to all obligations
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 77a6ee79cc..9219aa21ca 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -311,7 +311,7 @@ Summary of the commands
 
          This command has no effect when used on a typeclass.
 
-.. cmd:: Instance @ident {? @binders} : @class t1 … tn [| priority] := { field1 := b1 ; …; fieldi := bi }
+.. cmd:: Instance @ident {? @binders} : @class t1 … tn {? | priority } := { field1 := b1 ; …; fieldi := bi }
 
    This command is used to declare a typeclass instance named
    :token:`ident` of the class :token:`class` with parameters ``t1`` to ``tn`` and
@@ -324,7 +324,7 @@ Summary of the commands
    :tacn:`auto` hints. If the priority is not specified, it defaults to the number
    of non-dependent binders of the instance.
 
-   .. cmdv:: Instance @ident {? @binders} : forall {? @binders}, @class @term__1 … @term__n [| priority] := @term
+   .. cmdv:: Instance @ident {? @binders} : forall {? @binders}, @class @term__1 … @term__n {? | priority } := @term
 
       This syntax is used for declaration of singleton class instances or
       for directly giving an explicit term of type :n:`forall @binders, @class
@@ -356,7 +356,7 @@ Summary of the commands
 Besides the :cmd:`Class` and :cmd:`Instance` vernacular commands, there are a
 few other commands related to typeclasses.
 
-.. cmd:: Existing Instance {+ @ident} [| priority]
+.. cmd:: Existing Instance {+ @ident} {? | priority }
 
    This command adds an arbitrary list of constants whose type ends with
    an applied typeclass to the instance database with an optional
@@ -579,7 +579,7 @@ Settings
 Typeclasses eauto `:=`
 ~~~~~~~~~~~~~~~~~~~~~~
 
-.. cmd:: Typeclasses eauto := {? debug} {? (dfs) | (bfs) } @num
+.. cmd:: Typeclasses eauto := {? debug} {? {| (dfs) | (bfs) } } @num
    :name: Typeclasses eauto
 
    This command allows more global customization of the typeclass
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index cca3b2e06b..5e337bcef0 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -498,7 +498,7 @@ Other changes in 8.10+beta1
   - Command :cmd:`Instance`, when no body is provided, now always opens
     a proof. This is a breaking change, as instance of :n:`Instance
     @ident__1 : @ident__2.` where :n:`@ident__2` is a trivial class will
-    have to be changed into :n:`Instance @ident__1 : @ident__2 := {}.`
+    have to be changed into :n:`Instance @ident__1 : @ident__2 := %{%}.`
     or :n:`Instance @ident__1 : @ident__2. Proof. Qed.`
     (`#9274 <https://github.com/coq/coq/pull/9274>`_, by Maxime Dénès).
 
@@ -3940,7 +3940,7 @@ Vernacular commands
   Equality Schemes", this replaces deprecated option "Equality Scheme").
 - Made support for automatic generation of case analysis schemes available
   to user (governed by option "Set Case Analysis Schemes").
-- New command :n:`{? Global } Generalizable [All|No] [Variable|Variables] {* @ident}` to
+- New command :n:`{? Global } Generalizable {| All | No } {| Variable | Variables } {* @ident}` to
   declare which identifiers are generalizable in `` `{} `` and `` `() `` binders.
 - New command "Print Opaque Dependencies" to display opaque constants in
   addition to all variables, parameters or axioms a theorem or
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index ba766c8c3d..ccd25ec9f3 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -931,7 +931,7 @@ In the syntax of module application, the ! prefix indicates that any
    :token:`module_binding`. The output module type
    is verified against each :token:`module_type`.
 
-.. cmdv:: Module [ Import | Export ]
+.. cmdv:: Module {| Import | Export }
 
    Behaves like :cmd:`Module`, but automatically imports or exports the module.
 
@@ -1648,7 +1648,7 @@ Declaring Implicit Arguments
 
 
 
-.. cmd:: Arguments @qualid {* [ @ident ] | { @ident } | @ident }
+.. cmd:: Arguments @qualid {* {| [ @ident ] | { @ident } | @ident } }
    :name: Arguments (implicits)
 
    This command is used to set implicit arguments *a posteriori*,
@@ -1665,20 +1665,20 @@ Declaring Implicit Arguments
 
    This command clears implicit arguments.
 
-.. cmdv:: Global Arguments @qualid {* [ @ident ] | { @ident } | @ident }
+.. cmdv:: Global Arguments @qualid {* {| [ @ident ] | { @ident } | @ident } }
 
    This command is used to recompute the implicit arguments of
    :token:`qualid` after ending of the current section if any, enforcing the
    implicit arguments known from inside the section to be the ones
    declared by the command.
 
-.. cmdv:: Local Arguments @qualid {* [ @ident ] | { @ident } | @ident }
+.. cmdv:: Local Arguments @qualid {* {| [ @ident ] | { @ident } | @ident } }
 
    When in a module, tell not to activate the
    implicit arguments of :token:`qualid` declared by this command to contexts that
    require the module.
 
-.. cmdv:: {? Global | Local } Arguments @qualid {*, {+ [ @ident ] | { @ident } | @ident } }
+.. cmdv:: {? {| Global | Local } } Arguments @qualid {*, {+ {| [ @ident ] | { @ident } | @ident } } }
 
    For names of constants, inductive types,
    constructors, lemmas which can only be applied to a fixed number of
@@ -2167,7 +2167,7 @@ that specify which variables should be generalizable.
 
    Disable implicit generalization  entirely. This is the default behavior.
 
-.. cmd:: Generalizable (Variable | Variables) {+ @ident }
+.. cmd:: Generalizable {| Variable | Variables } {+ @ident }
 
    Allow generalization of the given identifiers only. Calling this command multiple times
    adds to the allowed identifiers.
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index 6e33862b39..aa603fc966 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -668,7 +668,7 @@ A scope is a name given to a grammar entry used to produce some Ltac2 expression
 at parsing time. Scopes are described using a form of S-expression.
 
 .. prodn::
-   ltac2_scope ::= @string %| @integer %| @lident ({+, @ltac2_scope})
+   ltac2_scope ::= {| @string | @integer | @lident ({+, @ltac2_scope}) }
 
 A few scopes contain antiquotation features. For sake of uniformity, all
 antiquotations are introduced by the syntax :n:`$@lident`.
@@ -751,7 +751,7 @@ Notations
 
 The Ltac2 parser can be extended by syntactic notations.
 
-.. cmd:: Ltac2 Notation {+ @lident (@ltac2_scope) %| @string } {? : @integer} := @ltac2_term
+.. cmd:: Ltac2 Notation {+ {| @lident (@ltac2_scope) | @string } } {? : @integer} := @ltac2_term
    :name: Ltac2 Notation
 
    A Ltac2 notation adds a parsing rule to the Ltac2 grammar, which is expanded
@@ -823,9 +823,9 @@ Ltac2 features a toplevel loop that can be used to evaluate expressions.
 Debug
 -----
 
-.. opt:: Ltac2 Backtrace
+.. flag:: Ltac2 Backtrace
 
-   When this option is set, toplevel failures will be printed with a backtrace.
+   When this flag is set, toplevel failures will be printed with a backtrace.
 
 Compatibility layer with Ltac1
 ------------------------------
@@ -966,7 +966,7 @@ errors produced by the typechecker.
 In Ltac expressions
 +++++++++++++++++++
 
-.. exn:: Unbound ( value | constructor ) X
+.. exn:: Unbound {| value | constructor } X
 
    * if `X` is meant to be a term from the current stactic environment, replace
      the problematic use by `'X`.
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 16b158c397..139506723e 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -322,7 +322,7 @@ Navigation in the proof tree
 .. index:: {
            }
 
-.. cmd:: %{ %| %}
+.. cmd:: {| %{ | %} }
 
    The command ``{`` (without a terminating period) focuses on the first
    goal, much like :cmd:`Focus` does, however, the subproof can only be
@@ -430,7 +430,7 @@ not go beyond enclosing ``{`` and ``}``, so bullets can be reused as further
 nesting levels provided they are delimited by these. Bullets are made of
 repeated ``-``, ``+`` or ``*`` symbols:
 
-.. prodn:: bullet ::= {+ - } %| {+ + } %| {+ * }
+.. prodn:: bullet ::= {| {+ - } | {+ + } | {+ * } }
 
 Note again that when a focused goal is proved a message is displayed
 together with a suggestion about the right bullet or ``}`` to unfocus it
@@ -492,7 +492,7 @@ The following example script illustrates all these features:
 
 Set Bullet Behavior
 ```````````````````
-.. opt:: Bullet Behavior  %( "None" %| "Strict Subproofs" %)
+.. opt:: Bullet Behavior {| "None" | "Strict Subproofs" }
    :name: Bullet Behavior
 
    This option controls the bullet behavior and can take two possible values:
@@ -680,7 +680,7 @@ This image shows an error message with diff highlighting in CoqIDE:
 How to enable diffs
 ```````````````````
 
-.. opt:: Diffs %( "on" %| "off" %| "removed" %)
+.. opt:: Diffs {| "on" | "off" | "removed" }
    :name: Diffs
 
    The “on” setting highlights added tokens in green, while the “removed” setting
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 4e40df6f94..d6247d1bc5 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -617,7 +617,7 @@ Abbreviations
      selected occurrences of a term.
 
 .. prodn::
-   occ_switch ::= { {? + %| - } {* @num } }
+   occ_switch ::= { {? {| + | - } } {* @num } }
 
 where:
 
@@ -2273,7 +2273,7 @@ to the others.
 Iteration
 ~~~~~~~~~
 
-.. tacn:: do {? @num } ( @tactic | [ {+| @tactic } ] )
+.. tacn:: do {? @num } {| @tactic | [ {+| @tactic } ] }
    :name: do (ssreflect)
 
    This tactical offers an accurate control on the repetition of tactics.
@@ -2300,7 +2300,7 @@ tactic should be repeated on the current subgoal.
 There are four kinds of multipliers:
 
 .. prodn::
-   mult ::= @num ! %| ! %| @num ? %| ?
+   mult ::= {| @num ! | ! | @num ? | ? }
 
 Their meaning is:
 
@@ -5444,7 +5444,7 @@ equivalences are indeed taken into account, otherwise only single
 |SSR| searching tool
 --------------------
 
-.. cmd:: Search {? @pattern }  {* {? - } %( @string %| @pattern %) {? % @ident} } {? in {+ {? - } @qualid } }
+.. cmd:: Search {? @pattern }  {* {? - } {| @string | @pattern } {? % @ident} } {? in {+ {? - } @qualid } }
    :name: Search (ssreflect)
 
    This is the |SSR| extension of the Search command. :token:`qualid` is the
@@ -5686,7 +5686,7 @@ respectively.
 
    local cofix definition
 
-.. tacn:: set @ident {? : @term } := {? @occ_switch } %( @term %| ( @c_pattern) %)
+.. tacn:: set @ident {? : @term } := {? @occ_switch } {| @term | ( @c_pattern) }
 
    abbreviation (see :ref:`abbreviations_ssr`)
 
@@ -5714,26 +5714,26 @@ introduction see :ref:`introduction_ssr`
 
 localization see :ref:`localization_ssr`
 
-.. prodn:: tactic += do {? @mult } %( @tactic %| [ {+| @tactic } ] %)
+.. prodn:: tactic += do {? @mult } {| @tactic | [ {+| @tactic } ] }
 
 iteration  see :ref:`iteration_ssr`
 
-.. prodn:: tactic += @tactic ; %( first %| last %) {? @num } %( @tactic %| [ {+| @tactic } ] %)
+.. prodn:: tactic += @tactic ; {| first | last } {? @num } {| @tactic | [ {+| @tactic } ] }
 
 selector  see :ref:`selectors_ssr`
 
-.. prodn:: tactic += @tactic ; %( first %| last %) {? @num }
+.. prodn:: tactic += @tactic ; {| first | last } {? @num }
 
 rotation see :ref:`selectors_ssr`
 
-.. prodn:: tactic += by %( @tactic %| [ {*| @tactic } ] %)
+.. prodn:: tactic += by {| @tactic | [ {*| @tactic } ] }
 
 closing see :ref:`terminators_ssr`
 
 Commands
 ~~~~~~~~
 
-.. cmd:: Hint View for %( move %| apply %) / @ident {? | @num }
+.. cmd:: Hint View for {| move | apply } / @ident {? | @num }
 
    view hint declaration (see :ref:`declaring_new_hints_ssr`)
 
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index c728b925ac..537a40c53c 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -3777,8 +3777,8 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
       discrimination network to relax or constrain it in the case of discriminated
       databases.
 
-   .. cmdv:: Hint Variables %( Transparent %| Opaque %) : @ident
-             Hint Constants %( Transparent %| Opaque %) : @ident
+   .. cmdv:: Hint Variables {| Transparent | Opaque } : @ident
+             Hint Constants {| Transparent | Opaque } : @ident
       :name: Hint Variables; Hint Constants
 
       This sets the transparency flag used during unification of
@@ -3850,7 +3850,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
       semantics of :n:`Hint Cut @regexp` is to set the cut expression
       to :n:`c | regexp`, the initial cut expression being `emp`.
 
-   .. cmdv:: Hint Mode @qualid {* (+ | ! | -)} : @ident
+   .. cmdv:: Hint Mode @qualid {* {| + | ! | - } } : @ident
       :name: Hint Mode
 
       This sets an optional mode of use of the identifier :n:`@qualid`. When
@@ -4016,7 +4016,7 @@ We propose a smooth transitional path by providing the :opt:`Loose Hint Behavior
 option which accepts three flags allowing for a fine-grained handling of
 non-imported hints.
 
-.. opt:: Loose Hint Behavior %( "Lax" %| "Warn" %| "Strict" %)
+.. opt:: Loose Hint Behavior {| "Lax" | "Warn" | "Strict" }
    :name: Loose Hint Behavior
 
    This option accepts three values, which control the behavior of hints w.r.t.
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index e207a072cc..4e4a10f590 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -91,13 +91,13 @@ and tables:
 Flags, options and tables are identified by a series of identifiers, each with an initial
 capital letter.
 
-.. cmd::  {? Local | Global | Export } Set @flag
+.. cmd::  {? {| Local | Global | Export } } Set @flag
    :name: Set
 
    Sets :token:`flag` on. Scoping qualifiers are
    described :ref:`here <set_unset_scope_qualifiers>`.
 
-.. cmd:: {? Local | Global | Export } Unset @flag
+.. cmd:: {? {| Local | Global | Export } } Unset @flag
    :name: Unset
 
    Sets :token:`flag` off. Scoping qualifiers are
@@ -108,13 +108,13 @@ capital letter.
    Prints the current value of :token:`flag`.
 
 
-.. cmd:: {? Local | Global | Export } Set @option ( @num | @string )
+.. cmd:: {? {| Local | Global | Export } } Set @option {| @num | @string }
    :name: Set @option
 
    Sets :token:`option` to the specified value.  Scoping qualifiers are
    described :ref:`here <set_unset_scope_qualifiers>`.
 
-.. cmd:: {? Local | Global | Export } Unset @option
+.. cmd:: {? {| Local | Global | Export } } Unset @option
    :name: Unset @option
 
    Sets :token:`option` to its default value.  Scoping qualifiers are
@@ -129,17 +129,17 @@ capital letter.
    Prints the current value of all flags and options, and the names of all tables.
 
 
-.. cmd:: Add @table ( @string | @qualid )
+.. cmd:: Add @table {| @string | @qualid }
    :name: Add @table
 
    Adds the specified value to :token:`table`.
 
-.. cmd:: Remove @table ( @string | @qualid )
+.. cmd:: Remove @table {| @string | @qualid }
    :name: Remove @table
 
    Removes the specified value from :token:`table`.
 
-.. cmd:: Test @table for ( @string | @qualid )
+.. cmd:: Test @table for {| @string | @qualid }
    :name: Test @table for
 
    Reports whether :token:`table` contains the specified value.
@@ -162,7 +162,7 @@ capital letter.
 Scope qualifiers for :cmd:`Set` and :cmd:`Unset`
 `````````````````````````````````````````````````
 
-:n:`{? Local | Global | Export }`
+:n:`{? {| Local | Global | Export } }`
 
 Flag and option settings can be global in scope or local to nested scopes created by
 :cmd:`Module` and :cmd:`Section` commands.  There are four alternatives:
@@ -622,7 +622,7 @@ file is a particular case of module called *library file*.
       but if a further module, say `A`, contains a command :cmd:`Require Export` `B`,
       then the command :cmd:`Require Import` `A` also imports the module `B.`
 
-   .. cmdv:: Require [Import | Export] {+ @qualid }
+   .. cmdv:: Require {| Import | Export } {+ @qualid }
 
       This loads the
       modules named by the :token:`qualid` sequence and their recursive
@@ -988,7 +988,7 @@ Controlling display
 
    This option controls the normal displaying.
 
-.. opt:: Warnings "{+, {? %( - %| + %) } @ident }"
+.. opt:: Warnings "{+, {? {| - | + } } @ident }"
    :name: Warnings
 
    This option configures the display of warnings. It is experimental, and
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 0ade9fdbf5..4bdfac7c42 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -39,14 +39,29 @@ from sphinx.ext import mathbase
 from . import coqdoc
 from .repl import ansicolors
 from .repl.coqtop import CoqTop, CoqTopError
+from .notations.parsing import ParseError
 from .notations.sphinx import sphinxify
 from .notations.plain import stringify_with_ellipses
 
-def parse_notation(notation, source, line, rawtext=None):
+PARSE_ERROR = """Parse error in notation!
+Offending notation: {}
+Error message: {}"""
+
+def notation_to_sphinx(notation, source, line, rawtext=None):
     """Parse notation and wrap it in an inline node"""
-    node = nodes.inline(rawtext or notation, '', *sphinxify(notation), classes=['notation'])
-    node.source, node.line = source, line
-    return node
+    try:
+        node = nodes.inline(rawtext or notation, '', *sphinxify(notation), classes=['notation'])
+        node.source, node.line = source, line
+        return node
+    except ParseError as e:
+        raise ExtensionError(PARSE_ERROR.format(notation, e.msg)) from e
+
+def notation_to_string(notation):
+    """Parse notation and format it as a string with ellipses."""
+    try:
+        return stringify_with_ellipses(notation)
+    except ParseError as e:
+        raise ExtensionError(PARSE_ERROR.format(notation, e.msg)) from e
 
 def highlight_using_coqdoc(sentence):
     """Lex sentence using coqdoc, and yield inline nodes for each token"""
@@ -136,7 +151,7 @@ class CoqObject(ObjectDescription):
         self._render_signature(signature, signode)
         name = self._names.get(signature)
         if name is None:
-            name = self._name_from_signature(signature)
+            name = self._name_from_signature(signature) # pylint: disable=assignment-from-none
             # remove trailing ‘.’ found in commands, but not ‘...’ (ellipsis)
             if name is not None and name.endswith(".") and not name.endswith("..."):
                 name = name[:-1]
@@ -241,7 +256,7 @@ class NotationObject(DocumentableObject):
     """
     def _render_signature(self, signature, signode):
         position = self.state_machine.get_source_and_line(self.lineno)
-        tacn_node = parse_notation(signature, *position)
+        tacn_node = notation_to_sphinx(signature, *position)
         signode += addnodes.desc_name(signature, '', tacn_node)
 
 class GallinaObject(PlainObject):
@@ -346,7 +361,7 @@ class OptionObject(NotationObject):
     annotation = "Option"
 
     def _name_from_signature(self, signature):
-        return stringify_with_ellipses(signature)
+        return notation_to_string(signature)
 
 
 class FlagObject(NotationObject):
@@ -365,7 +380,7 @@ class FlagObject(NotationObject):
     annotation = "Flag"
 
     def _name_from_signature(self, signature):
-        return stringify_with_ellipses(signature)
+        return notation_to_string(signature)
 
 
 class TableObject(NotationObject):
@@ -383,7 +398,7 @@ class TableObject(NotationObject):
     annotation = "Table"
 
     def _name_from_signature(self, signature):
-        return stringify_with_ellipses(signature)
+        return notation_to_string(signature)
 
 class ProductionObject(CoqObject):
     r"""A grammar production.
@@ -403,7 +418,7 @@ class ProductionObject(CoqObject):
     Example::
 
         .. prodn:: term += let: @pattern := @term in @term
-        .. prodn:: occ_switch ::= { {? + %| - } {* @num } }
+        .. prodn:: occ_switch ::= { {? {| + | - } } {* @num } }
 
     """
     subdomain = "prodn"
@@ -432,7 +447,7 @@ class ProductionObject(CoqObject):
         lhs_node = nodes.literal(lhs_op, lhs_op)
 
         position = self.state_machine.get_source_and_line(self.lineno)
-        rhs_node = parse_notation(rhs, *position)
+        rhs_node = notation_to_sphinx(rhs, *position)
         signode += addnodes.desc_name(signature, '', lhs_node, rhs_node)
 
         return ('token', lhs) if op == '::=' else None
@@ -475,7 +490,7 @@ class ExceptionObject(NotationObject):
 
     # Generate names automatically
     def _name_from_signature(self, signature):
-        return stringify_with_ellipses(signature)
+        return notation_to_string(signature)
 
 class WarningObject(NotationObject):
     """An warning raised by a Coq command or tactic..
@@ -497,7 +512,7 @@ class WarningObject(NotationObject):
 
     # Generate names automatically
     def _name_from_signature(self, signature):
-        return stringify_with_ellipses(signature)
+        return notation_to_string(signature)
 
 def NotationRole(role, rawtext, text, lineno, inliner, options={}, content=[]):
     #pylint: disable=unused-argument, dangerous-default-value
@@ -516,7 +531,7 @@ def NotationRole(role, rawtext, text, lineno, inliner, options={}, content=[]):
     """
     notation = utils.unescape(text, 1)
     position = inliner.reporter.get_source_and_line(lineno)
-    return [nodes.literal(rawtext, '', parse_notation(notation, *position, rawtext=rawtext))], []
+    return [nodes.literal(rawtext, '', notation_to_sphinx(notation, *position, rawtext=rawtext))], []
 
 def coq_code_role(role, rawtext, text, lineno, inliner, options={}, content=[]):
     #pylint: disable=dangerous-default-value
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/parsing.py b/doc/tools/coqrst/notations/parsing.py
index 506240d907..2312e09090 100644
--- a/doc/tools/coqrst/notations/parsing.py
+++ b/doc/tools/coqrst/notations/parsing.py
@@ -11,10 +11,22 @@ from .TacticNotationsLexer import TacticNotationsLexer
 from .TacticNotationsParser import TacticNotationsParser
 
 from antlr4 import CommonTokenStream, InputStream
+from antlr4.error.ErrorListener import ErrorListener
 
 SUBSTITUTIONS = [#("@bindings_list", "{+ (@id := @val) }"),
                  ("@qualid_or_string", "@id|@string")]
 
+class ParseError(Exception):
+    def __init__(self, msg):
+        super().__init__()
+        self.msg = msg
+
+class ExceptionRaisingErrorListener(ErrorListener):
+    def syntaxError(self, recognizer, offendingSymbol, line, column, msg, e):
+        raise ParseError("{}:{}: {}".format(line, column, msg))
+
+ERROR_LISTENER = ExceptionRaisingErrorListener()
+
 def substitute(notation):
     """Perform common substitutions in the notation string.
 
@@ -27,11 +39,13 @@ def substitute(notation):
     return notation
 
 def parse(notation):
-    """Parse a notation string.
+    """Parse a notation string, optionally reporting errors to `error_listener`.
 
     :return: An ANTLR AST. Use one of the supplied visitors (or write your own)
              to turn it into useful output.
     """
     substituted = substitute(notation)
     lexer = TacticNotationsLexer(InputStream(substituted))
-    return TacticNotationsParser(CommonTokenStream(lexer)).top()
+    parser = TacticNotationsParser(CommonTokenStream(lexer))
+    parser.addErrorListener(ERROR_LISTENER)
+    return parser.top()
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))