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

Reviewed-by: Zimmi48
Ack-by: jfehrle

5 files changed, 33 insertions, 33 deletions

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