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

Reviewed-by: Zimmi48
Ack-by: jfehrle

15 files changed, 121 insertions, 57 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