Remove unneeded | in productionlists

10 files changed, 265 insertions, 265 deletions

diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst
index e468cc63cd..b606fb4dd2 100644
--- a/doc/sphinx/addendum/generalized-rewriting.rst
+++ b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -714,47 +714,47 @@ following grammar:
 
 .. productionlist:: rewriting
    s, t, u : `strategy`
-           : | `lemma`
-           : | `lemma_right_to_left`
-           : | `failure`
-           : | `identity`
-           : | `reflexivity`
-           : | `progress`
-           : | `failure_catch`
-           : | `composition`
-           : | `left_biased_choice`
-           : | `iteration_one_or_more`
-           : | `iteration_zero_or_more`
-           : | `one_subterm`
-           : | `all_subterms`
-           : | `innermost_first`
-           : | `outermost_first`
-           : | `bottom_up`
-           : | `top_down`
-           : | `apply_hint`
-           : | `any_of_the_terms`
-           : | `apply_reduction`
-           : | `fold_expression`
+           : `lemma`
+           : `lemma_right_to_left`
+           : `failure`
+           : `identity`
+           : `reflexivity`
+           : `progress`
+           : `failure_catch`
+           : `composition`
+           : `left_biased_choice`
+           : `iteration_one_or_more`
+           : `iteration_zero_or_more`
+           : `one_subterm`
+           : `all_subterms`
+           : `innermost_first`
+           : `outermost_first`
+           : `bottom_up`
+           : `top_down`
+           : `apply_hint`
+           : `any_of_the_terms`
+           : `apply_reduction`
+           : `fold_expression`
 
 .. productionlist:: rewriting
-   strategy : "(" `s` ")"
+   strategy : ( `s` )
    lemma : `c`
-   lemma_right_to_left : "<-" `c`
-   failure : `fail`
-   identity : `id`
-   reflexivity : `refl`
-   progress : `progress` `s`
-   failure_catch : `try` `s`
-   composition : `s` ";" `u`
+   lemma_right_to_left : <- `c`
+   failure : fail
+   identity : id
+   reflexivity : refl
+   progress : progress `s`
+   failure_catch : try `s`
+   composition : `s` ; `u`
    left_biased_choice : choice `s` `t`
-   iteration_one_or_more : `repeat` `s`
-   iteration_zero_or_more : `any` `s`
+   iteration_one_or_more : repeat `s`
+   iteration_zero_or_more : any `s`
    one_subterm : subterm `s`
    all_subterms : subterms `s`
-   innermost_first : `innermost` `s`
-   outermost_first : `outermost` `s`
-   bottom_up : `bottomup` `s`
-   top_down : `topdown` `s`
+   innermost_first : innermost `s`
+   outermost_first : outermost `s`
+   bottom_up : bottomup `s`
+   top_down : topdown `s`
    apply_hint : hints `hintdb`
    any_of_the_terms : terms (`c`)+
    apply_reduction : eval `redexpr`
@@ -767,7 +767,7 @@ primitive fixpoint operator:
 .. productionlist:: rewriting
    try `s` : choice `s` `id`
    any `s` : fix `u`. try (`s` ; `u`)
-   repeat `s` : `s` ; `any` `s`
+   repeat `s` : `s` ; any `s`
    bottomup s : fix `bu`. (choice (progress (subterms bu)) s) ; try bu
    topdown s : fix `td`. (choice s (progress (subterms td))) ; try td
    innermost s : fix `i`. (choice (subterm i) s)
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index 64e2d7c4ab..e5b41be691 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -41,8 +41,8 @@ Formally, the syntax of a classes is defined as:
 
 .. productionlist::
    class: `qualid`
-        : | Sortclass
-        : | Funclass
+        : Sortclass
+        : Funclass
 
 
 Coercions
@@ -184,10 +184,10 @@ Figure :ref:`vernacular` as follows:
    \comindex{Hypothesis \mbox{\rm (and coercions)}}
 
 .. productionlist::
-   assumption : assumption_keyword assums .
-   assums : simple_assums
-          : | (simple_assums) ... (simple_assums)
-   simple_assums : ident ... ident :[>] term
+   assumption : `assumption_keyword` `assums` .
+   assums : `simple_assums`
+          : (`simple_assums`) ... (`simple_assums`)
+   simple_assums : `ident` ... `ident` :[>] `term`
 
 If the extra ``>`` is present before the type of some assumptions, these
 assumptions are declared as coercions.
@@ -203,7 +203,7 @@ grammar of inductive types from Figure :ref:`vernacular` as follows:
 
 .. productionlist::
    inductive : Inductive `ind_body` with ... with `ind_body`
-             : | CoInductive `ind_body` with ... with `ind_body`
+             : CoInductive `ind_body` with ... with `ind_body`
    ind_body : `ident` [ `binders` ] : `term` := [[|] `constructor` | ... | `constructor` ]
    constructor : `ident` [ `binders` ] [:[>] `term` ]
 
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index fd66de427c..e799677c59 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -38,7 +38,7 @@ The tactics solve propositional formulas parameterized by atomic
 arithmetic expressions interpreted over a domain :math:`D \in \{\mathbb{Z},\mathbb{Q},\mathbb{R}\}`.
 The syntax of the formulas is the following:
 
- .. productionlist:: `F`
+ .. productionlist:: F
    F : A ∣ P ∣ True ∣ False ∣ F ∧ F ∣ F ∨ F ∣ F ↔ F ∣ F → F ∣ ¬ F
    A : p = p ∣ p > p ∣ p < p ∣ p ≥ p ∣ p ≤ p
    p : c ∣ x ∣ −p ∣ p − p ∣ p + p ∣ p × p ∣ p ^ n
diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst
index 99d689132d..8204d93fa7 100644
--- a/doc/sphinx/addendum/ring.rst
+++ b/doc/sphinx/addendum/ring.rst
@@ -308,13 +308,13 @@ The syntax for adding a new ring is
 
    .. productionlist:: coq
       ring_mod : abstract | decidable `term` | morphism `term`
-               : | setoid `term` `term`
-               : | constants [`ltac`]
-               : | preprocess [`ltac`]
-               : | postprocess [`ltac`]
-               : | power_tac `term` [`ltac`]
-               : | sign `term`
-               : | div `term`
+               : setoid `term` `term`
+               : constants [`ltac`]
+               : preprocess [`ltac`]
+               : postprocess [`ltac`]
+               : power_tac `term` [`ltac`]
+               : sign `term`
+               : div `term`
 
    abstract
       declares the ring as abstract. This is the default.
diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst
index 10650af1d1..b82b3b0e80 100644
--- a/doc/sphinx/language/coq-library.rst
+++ b/doc/sphinx/language/coq-library.rst
@@ -104,18 +104,18 @@ subclass :token:`form` of the syntactic class :token:`term`. The syntax of
    a nice last column. Or even better, find a proper way to do this!
 
 .. productionlist::
-   form :   True                                           (True)
-        : | False                                          (False)
-        : | ~ `form`                                         (not)
-        : | `form` /\ `form`                                   (and)
-        : | `form` \/ `form`                                   (or)
-        : | `form` -> `form`                                   (primitive implication)
-        : | `form` <-> `form`                                  (iff)
-        : | forall `ident` : `type`, `form`                      (primitive for all)
-        : | exists `ident` [: `specif`], `form`                  (ex)
-        : | exists2 `ident` [: `specif`], `form` & `form`          (ex2)
-        : | `term` = `term`                                    (eq)
-        : | `term` = `term` :> `specif`                          (eq)
+   form : True                                           (True)
+        : False                                          (False)
+        : ~ `form`                                         (not)
+        : `form` /\ `form`                                   (and)
+        : `form` \/ `form`                                   (or)
+        : `form` -> `form`                                   (primitive implication)
+        : `form` <-> `form`                                  (iff)
+        : forall `ident` : `type`, `form`                      (primitive for all)
+        : exists `ident` [: `specif`], `form`                  (ex)
+        : exists2 `ident` [: `specif`], `form` & `form`          (ex2)
+        : `term` = `term`                                    (eq)
+        : `term` = `term` :> `specif`                          (eq)
 
 .. note::
 
@@ -287,13 +287,13 @@ the next section :ref:`specification`):
 
 .. productionlist::
    specif :  `specif` * `specif`                           (prod)
-          : | `specif` + `specif`                          (sum)
-          : | `specif` + { `specif` }                      (sumor)
-          : | { `specif` } + { `specif` }                  (sumbool)
-          : | { `ident` : `specif` | `form` }              (sig)
-          : | { `ident` : `specif` | `form` & `form` }       (sig2)
-          : | { `ident` : `specif` & `specif` }             (sigT)
-          : | { `ident` : `specif` & `specif` & `specif` }    (sigT2)
+          : `specif` + `specif`                          (sum)
+          : `specif` + { `specif` }                      (sumor)
+          : { `specif` } + { `specif` }                  (sumbool)
+          : { `ident` : `specif` | `form` }              (sig)
+          : { `ident` : `specif` | `form` & `form` }       (sig2)
+          : { `ident` : `specif` & `specif` }             (sigT)
+          : { `ident` : `specif` & `specif` & `specif` }    (sigT2)
   term : (`term`, `term`)                               (pair)
 
 
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 376a6b8eed..d0e44cd212 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -25,7 +25,7 @@ expressions. In this sense, the :cmd:`Record` construction allows defining
      record_keyword : Record | Inductive | CoInductive
      record_body    : `ident` [ `binders` ] [: `sort` ] := [ `ident` ] { [ `field` ; … ; `field` ] }.
      field          : `ident` [ `binders` ] : `type` [ where `notation` ]
-                    : | `ident` [ `binders` ] [: `type` ] := `term`
+                    : `ident` [ `binders` ] [: `type` ] := `term`
 
 .. cmd:: Record @ident @binders {? : @sort} := {? @ident} { {*; @ident @binders : @type } }
 
@@ -165,8 +165,8 @@ available:
 
   .. productionlist:: terms
      projection : `term` `.` ( `qualid` )
-          : | `term` `.` ( `qualid` `arg` … `arg` )
-          : | `term` `.` ( @`qualid` `term` … `term` )
+          : `term` `.` ( `qualid` `arg` … `arg` )
+          : `term` `.` ( @`qualid` `term` … `term` )
 
   Syntax of Record projections
 
@@ -818,14 +818,14 @@ together, as well as a means of massive abstraction.
 
   .. productionlist:: modules
     module_type       : `qualid`
-                      : | `module_type` with Definition `qualid` := `term`
-                      : | `module_type` with Module `qualid` := `qualid`
-                      : | `qualid` `qualid` … `qualid`
-                      : | !`qualid` `qualid` … `qualid`
+                      : `module_type` with Definition `qualid` := `term`
+                      : `module_type` with Module `qualid` := `qualid`
+                      : `qualid` `qualid` … `qualid`
+                      : !`qualid` `qualid` … `qualid`
     module_binding    : ( [Import|Export] `ident` … `ident` : `module_type` )
     module_bindings   : `module_binding` … `module_binding`
     module_expression : `qualid` … `qualid`
-                      : | !`qualid` … `qualid`
+                      : !`qualid` … `qualid`
 
   Syntax of modules
 
@@ -1814,10 +1814,10 @@ This syntax extension is given in the following grammar:
 
   .. productionlist:: explicit_apps
        term     : @ `qualid` `term` … `term`
-                : | @ `qualid`
-                : | `qualid` `argument` … `argument`
+                : @ `qualid`
+                : `qualid` `argument` … `argument`
        argument : `term`
-                : | (`ident` := `term`)
+                : (`ident` := `term`)
 
   Syntax for explicitly giving implicit arguments
 
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 8fa631174f..5ecf007eff 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -127,43 +127,43 @@ is described in Chapter :ref:`syntaxextensionsandinterpretationscopes`.
 
 .. productionlist:: coq
    term             : forall `binders` , `term`
-                    : | fun `binders` => `term`
-                    : | fix `fix_bodies`
-                    : | cofix `cofix_bodies`
-                    : | let `ident` [`binders`] [: `term`] := `term` in `term`
-                    : | let fix `fix_body` in `term`
-                    : | let cofix `cofix_body` in `term`
-                    : | let ( [`name` , … , `name`] ) [`dep_ret_type`] := `term` in `term`
-                    : | let ' `pattern` [in `term`] := `term` [`return_type`] in `term`
-                    : | if `term` [`dep_ret_type`] then `term` else `term`
-                    : | `term` : `term`
-                    : | `term` <: `term`
-                    : | `term` :>
-                    : | `term` -> `term`
-                    : | `term` `arg` … `arg`
-                    : | @ `qualid` [`term` … `term`]
-                    : | `term` % `ident`
-                    : | match `match_item` , … , `match_item` [`return_type`] with
+                    : fun `binders` => `term`
+                    : fix `fix_bodies`
+                    : cofix `cofix_bodies`
+                    : let `ident` [`binders`] [: `term`] := `term` in `term`
+                    : let fix `fix_body` in `term`
+                    : let cofix `cofix_body` in `term`
+                    : let ( [`name` , … , `name`] ) [`dep_ret_type`] := `term` in `term`
+                    : let ' `pattern` [in `term`] := `term` [`return_type`] in `term`
+                    : if `term` [`dep_ret_type`] then `term` else `term`
+                    : `term` : `term`
+                    : `term` <: `term`
+                    : `term` :>
+                    : `term` -> `term`
+                    : `term` `arg` … `arg`
+                    : @ `qualid` [`term` … `term`]
+                    : `term` % `ident`
+                    : match `match_item` , … , `match_item` [`return_type`] with
                     :   [[|] `equation` | … | `equation`] end
-                    : | `qualid`
-                    : | `sort`
-                    : | `num`
-                    : | _
-                    : | ( `term` )
+                    : `qualid`
+                    : `sort`
+                    : `num`
+                    : _
+                    : ( `term` )
    arg              : `term`
-                    : | ( `ident` := `term` )
+                    : ( `ident` := `term` )
    binders          : `binder` … `binder`
    binder           : `name`
-                    : | ( `name` … `name` : `term` )
-                    : | ( `name` [: `term`] := `term` )
-                    : | ' `pattern`
+                    : ( `name` … `name` : `term` )
+                    : ( `name` [: `term`] := `term` )
+                    : ' `pattern`
    name             : `ident` | _
    qualid           : `ident` | `qualid` `access_ident`
    sort             : Prop | Set | Type
    fix_bodies       : `fix_body`
-                    : | `fix_body` with `fix_body` with … with `fix_body` for `ident`
+                    : `fix_body` with `fix_body` with … with `fix_body` for `ident`
    cofix_bodies     : `cofix_body`
-                    : | `cofix_body` with `cofix_body` with … with `cofix_body` for `ident`
+                    : `cofix_body` with `cofix_body` with … with `cofix_body` for `ident`
    fix_body         : `ident` `binders` [`annotation`] [: `term`] := `term`
    cofix_body       : `ident` [`binders`] [: `term`] := `term`
    annotation       : { struct `ident` }
@@ -173,13 +173,13 @@ is described in Chapter :ref:`syntaxextensionsandinterpretationscopes`.
    equation         : `mult_pattern` | … | `mult_pattern` => `term`
    mult_pattern     : `pattern` , … , `pattern`
    pattern          : `qualid` `pattern` … `pattern`
-                    : | @ `qualid` `pattern` … `pattern`
-                    : | `pattern` as `ident`
-                    : | `pattern` % `ident`
-                    : | `qualid`
-                    : | _
-                    : | `num`
-                    : | ( `or_pattern` , … , `or_pattern` )
+                    : @ `qualid` `pattern` … `pattern`
+                    : `pattern` as `ident`
+                    : `pattern` % `ident`
+                    : `qualid`
+                    : _
+                    : `num`
+                    : ( `or_pattern` , … , `or_pattern` )
    or_pattern       : `pattern` | … | `pattern`
 
 
@@ -524,38 +524,38 @@ The Vernacular
 .. productionlist:: coq
    decorated-sentence : [ `decoration` … `decoration` ] `sentence`
    sentence           : `assumption`
-                      : | `definition`
-                      : | `inductive`
-                      : | `fixpoint`
-                      : | `assertion` `proof`
+                      : `definition`
+                      : `inductive`
+                      : `fixpoint`
+                      : `assertion` `proof`
    assumption         : `assumption_keyword` `assums`.
    assumption_keyword : Axiom | Conjecture
-                      : | Parameter | Parameters
-                      : | Variable | Variables
-                      : | Hypothesis | Hypotheses
+                      : Parameter | Parameters
+                      : Variable | Variables
+                      : Hypothesis | Hypotheses
    assums             : `ident` … `ident` : `term`
-                      : | ( `ident` … `ident` : `term` ) … ( `ident` … `ident` : `term` )
+                      : ( `ident` … `ident` : `term` ) … ( `ident` … `ident` : `term` )
    definition         : [Local] Definition `ident` [`binders`] [: `term`] := `term` .
-                      : | Let `ident` [`binders`] [: `term`] := `term` .
+                      : Let `ident` [`binders`] [: `term`] := `term` .
    inductive          : Inductive `ind_body` with … with `ind_body` .
-                      : | CoInductive `ind_body` with … with `ind_body` .
+                      : CoInductive `ind_body` with … with `ind_body` .
    ind_body           : `ident` [`binders`] : `term` :=
                       : [[|] `ident` [`binders`] [:`term`] | … | `ident` [`binders`] [:`term`]]
    fixpoint           : Fixpoint `fix_body` with … with `fix_body` .
-                      : | CoFixpoint `cofix_body` with … with `cofix_body` .
+                      : CoFixpoint `cofix_body` with … with `cofix_body` .
    assertion          : `assertion_keyword` `ident` [`binders`] : `term` .
    assertion_keyword  : Theorem | Lemma
-                      : | Remark | Fact
-                      : | Corollary | Proposition
-                      : | Definition | Example
+                      : Remark | Fact
+                      : Corollary | Proposition
+                      : Definition | Example
    proof              : Proof . … Qed .
-                      : | Proof . … Defined .
-                      : | Proof . … Admitted .
+                      : Proof . … Defined .
+                      : Proof . … Admitted .
    decoration : #[ `attributes` ]
    attributes : [`attribute`, … , `attribute`]
    attribute :  `ident`
-   :| `ident` = `string`
-   :| `ident` ( `attributes` )
+             : `ident` = `string`
+             : `ident` ( `attributes` )
 
 .. todo:: This use of … in this grammar is inconsistent
           What about removing the proof part of this grammar from this chapter
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 1071682ead..3629b5c5ec 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -70,88 +70,88 @@ mode but it can also be used in toplevel definitions as shown below.
 
 .. productionlist::  coq
    expr              : `expr` ; `expr`
-                     : | [> `expr` | ... | `expr` ]
-                     : | `expr` ; [ `expr` | ... | `expr` ]
-                     : | `tacexpr3`
-   tacexpr3          : do (`natural` | `ident`) tacexpr3
-                     : | progress `tacexpr3`
-                     : | repeat `tacexpr3`
-                     : | try `tacexpr3`
-                     : | once `tacexpr3`
-                     : | exactly_once `tacexpr3`
-                     : | timeout (`natural` | `ident`) `tacexpr3`
-                     : | time [`string`] `tacexpr3`
-                     : | only `selector`: `tacexpr3`
-                     : | `tacexpr2`
+                     : [> `expr` | ... | `expr` ]
+                     : `expr` ; [ `expr` | ... | `expr` ]
+                     : `tacexpr3`
+   tacexpr3          : do (`natural` | `ident`) `tacexpr3`
+                     : progress `tacexpr3`
+                     : repeat `tacexpr3`
+                     : try `tacexpr3`
+                     : once `tacexpr3`
+                     : exactly_once `tacexpr3`
+                     : timeout (`natural` | `ident`) `tacexpr3`
+                     : time [`string`] `tacexpr3`
+                     : only `selector`: `tacexpr3`
+                     : `tacexpr2`
    tacexpr2          : `tacexpr1` || `tacexpr3`
-                     : | `tacexpr1` + `tacexpr3`
-                     : | tryif `tacexpr1` then `tacexpr1` else `tacexpr1`
-                     : | `tacexpr1`
+                     : `tacexpr1` + `tacexpr3`
+                     : tryif `tacexpr1` then `tacexpr1` else `tacexpr1`
+                     : `tacexpr1`
    tacexpr1          : fun `name` ... `name` => `atom`
-                     : | let [rec] `let_clause` with ... with `let_clause` in `atom`
-                     : | match goal with `context_rule` | ... | `context_rule` end
-                     : | match reverse goal with `context_rule` | ... | `context_rule` end
-                     : | match `expr` with `match_rule` | ... | `match_rule` end
-                     : | lazymatch goal with `context_rule` | ... | `context_rule` end
-                     : | lazymatch reverse goal with `context_rule` | ... | `context_rule` end
-                     : | lazymatch `expr` with `match_rule` | ... | `match_rule` end
-                     : | multimatch goal with `context_rule` | ... | `context_rule` end
-                     : | multimatch reverse goal with `context_rule` | ... | `context_rule` end
-                     : | multimatch `expr` with `match_rule` | ... | `match_rule` end
-                     : | abstract `atom`
-                     : | abstract `atom` using `ident`
-                     : | first [ `expr` | ... | `expr` ]
-                     : | solve [ `expr` | ... | `expr` ]
-                     : | idtac [ `message_token` ... `message_token`]
-                     : | fail [`natural`] [`message_token` ... `message_token`]
-                     : | fresh [ `component` … `component` ]
-                     : | context `ident` [`term`]
-                     : | eval `redexpr` in `term`
-                     : | type of `term`
-                     : | constr : `term`
-                     : | uconstr : `term`
-                     : | type_term `term`
-                     : | numgoals
-                     : | guard `test`
-                     : | assert_fails `tacexpr3`
-                     : | assert_succeeds `tacexpr3`
-                     : | `atomic_tactic`
-                     : | `qualid` `tacarg` ... `tacarg`
-                     : | `atom`
+                     : let [rec] `let_clause` with ... with `let_clause` in `atom`
+                     : match goal with `context_rule` | ... | `context_rule` end
+                     : match reverse goal with `context_rule` | ... | `context_rule` end
+                     : match `expr` with `match_rule` | ... | `match_rule` end
+                     : lazymatch goal with `context_rule` | ... | `context_rule` end
+                     : lazymatch reverse goal with `context_rule` | ... | `context_rule` end
+                     : lazymatch `expr` with `match_rule` | ... | `match_rule` end
+                     : multimatch goal with `context_rule` | ... | `context_rule` end
+                     : multimatch reverse goal with `context_rule` | ... | `context_rule` end
+                     : multimatch `expr` with `match_rule` | ... | `match_rule` end
+                     : abstract `atom`
+                     : abstract `atom` using `ident`
+                     : first [ `expr` | ... | `expr` ]
+                     : solve [ `expr` | ... | `expr` ]
+                     : idtac [ `message_token` ... `message_token`]
+                     : fail [`natural`] [`message_token` ... `message_token`]
+                     : fresh [ `component` … `component` ]
+                     : context `ident` [`term`]
+                     : eval `redexpr` in `term`
+                     : type of `term`
+                     : constr : `term`
+                     : uconstr : `term`
+                     : type_term `term`
+                     : numgoals
+                     : guard `test`
+                     : assert_fails `tacexpr3`
+                     : assert_succeeds `tacexpr3`
+                     : `atomic_tactic`
+                     : `qualid` `tacarg` ... `tacarg`
+                     : `atom`
    atom              : `qualid`
-                     : | ()
-                     : | `integer`
-                     : | ( `expr` )
+                     : ()
+                     : `integer`
+                     : ( `expr` )
    component : `string` | `qualid`
    message_token     : `string` | `ident` | `integer`
    tacarg            : `qualid`
-                     : | ()
-                     : | ltac : `atom`
-                     : | `term`
+                     : ()
+                     : ltac : `atom`
+                     : `term`
    let_clause        : `ident` [`name` ... `name`] := `expr`
    context_rule      : `context_hyp`, ..., `context_hyp` |- `cpattern` => `expr`
-                     : | `cpattern` => `expr`
-                     : | |- `cpattern` => `expr`
-                     : | _ => `expr`
+                     : `cpattern` => `expr`
+                     : |- `cpattern` => `expr`
+                     : _ => `expr`
    context_hyp       : `name` : `cpattern`
-                     : | `name` := `cpattern` [: `cpattern`]
+                     : `name` := `cpattern` [: `cpattern`]
    match_rule        : `cpattern` => `expr`
-                     : | context [ident] [ `cpattern` ] => `expr`
-                     : | _ => `expr`
+                     : context [`ident`] [ `cpattern` ] => `expr`
+                     : _ => `expr`
    test              : `integer` = `integer`
-                     : | `integer` (< | <= | > | >=) `integer`
+                     : `integer` (< | <= | > | >=) `integer`
    selector          : [`ident`]
-                     : | `integer`
-                     : | (`integer` | `integer` - `integer`), ..., (`integer` | `integer` - `integer`)
+                     : `integer`
+                     : (`integer` | `integer` - `integer`), ..., (`integer` | `integer` - `integer`)
    toplevel_selector : `selector`
-                     : | all
-                     : | par
-                     : | !
+                     : all
+                     : par
+                     : !
 
 .. productionlist:: coq
    top              : [Local] Ltac `ltac_def` with ... with `ltac_def`
    ltac_def         : `ident` [`ident` ... `ident`] := `expr`
-                    : | `qualid` [`ident` ... `ident`] ::= `expr`
+                    : `qualid` [`ident` ... `ident`] ::= `expr`
 
 .. _ltac-semantics:
 
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 59602581c7..695e1ea833 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -36,7 +36,7 @@ language will be described in Chapter :ref:`ltac`.
 .. _invocation-of-tactics:
 
 Invocation of tactics
--------------------------
+~~~~~~~~~~~~~~~~~~~~~
 
 A tactic is applied as an ordinary command. It may be preceded by a
 goal selector (see Section :ref:`ltac-semantics`). If no selector is
@@ -44,9 +44,9 @@ specified, the default selector is used.
 
 .. _tactic_invocation_grammar:
 
-  .. productionlist:: `sentence`
-     tactic_invocation : toplevel_selector : tactic.
-                       : |tactic .
+  .. productionlist:: sentence
+     tactic_invocation : `toplevel_selector` : `tactic`.
+                       : `tactic` .
 
 .. opt:: Default Goal Selector "@toplevel_selector"
    :name: Default Goal Selector
@@ -79,14 +79,14 @@ bindings_list`` where ``bindings_list`` may be of two different forms:
 .. _bindings_list_grammar:
 
   .. productionlist:: `bindings_list`
-     bindings_list : (ref := `term`) ... (ref := `term`)
+     bindings_list : (`ref` := `term`) ... (`ref` := `term`)
                    : `term` ... `term`
 
-+ In a bindings list of the form :n:`{* (ref:= term)}`, :n:`ref` is either an
++ In a bindings list of the form :n:`{+ (@ref:= @term)}`, :n:`@ref` is either an
   :n:`@ident` or a :n:`@num`. The references are determined according to the type of
-  ``term``. If :n:`ref` is an identifier, this identifier has to be bound in the
+  ``term``. If :n:`@ref` is an identifier, this identifier has to be bound in the
   type of ``term`` and the binding provides the tactic with an instance for the
-  parameter of this name. If :n:`ref` is some number ``n``, this number denotes
+  parameter of this name. If :n:`@ref` is some number ``n``, this number denotes
   the ``n``-th non dependent premise of the ``term``, as determined by the type
   of ``term``.
 
@@ -113,11 +113,11 @@ Occurrence sets and occurrence clauses
 An occurrence clause is a modifier to some tactics that obeys the
 following syntax:
 
-  .. productionlist:: `sentence`
+  .. productionlist:: sentence
      occurrence_clause : in `goal_occurrences`
-     goal_occurrences : [`ident` [`at_occurrences`], ... , ident [`at_occurrences`] [|- [* [`at_occurrences`]]]]
-                      :| * |- [* [`at_occurrences`]]
-                      :| *
+     goal_occurrences : [`ident` [`at_occurrences`], ... , `ident` [`at_occurrences`] [|- [* [`at_occurrences`]]]]
+                      : * |- [* [`at_occurrences`]]
+                      : *
      at_occurrences : at `occurrences`
      occurrences     : [-] `num` ... `num`
 
@@ -3586,15 +3586,15 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
       the following. Beware, there is no operator precedence during parsing, one can
       check with :cmd:`Print HintDb` to verify the current cut expression:
 
-      .. productionlist:: `regexp`
-          e : ident      hint or instance identifier
-            :| _         any hint
-            :| e\|e′     disjunction
-            :| e e′      sequence
-            :| e *       Kleene star
-            :| emp       empty
-            :| eps       epsilon
-            :| ( e  )
+      .. productionlist:: regexp
+          e : `ident`    hint or instance identifier
+            : _          any hint
+            : `e` | `e`  disjunction
+            : `e` `e`    sequence
+            : `e` *      Kleene star
+            : emp        empty
+            : eps        epsilon
+            : ( `e` )
 
       The `emp` regexp does not match any search path while `eps`
       matches the empty path. During proof search, the path of
@@ -4299,15 +4299,15 @@ Automating
 
    .. _btauto_grammar:
 
-   .. productionlist:: `sentence`
-      t : x
-        :∣ true
-        :∣ false
-        :∣ orb t1 t2
-        :∣ andb t1 t2
-        :∣ xorb t1 t2
-        :∣ negb t
-        :∣ if t1 then t2 else t3
+   .. productionlist:: sentence
+      t : `x`
+        : true
+        : false
+        : orb `t` `t`
+        : andb `t` `t`
+        : xorb `t` `t`
+        : negb `t`
+        : if `t` then `t` else `t`
 
    Whenever the formula supplied is not a tautology, it also provides a
    counter-example.
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 47afa5ba0c..c707da1353 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -859,41 +859,41 @@ notations are given below. The optional :production:`scope` is described in
 
 .. productionlist:: coq
    notation      : [Local] Notation `string` := `term` [`modifiers`] [: `scope`].
-                 : | [Local] Infix `string` := `qualid` [`modifiers`] [: `scope`].
-                 : | [Local] Reserved Notation `string` [`modifiers`] .
-                 : | Inductive `ind_body` [`decl_notation`] with … with `ind_body` [`decl_notation`].
-                 : | CoInductive `ind_body` [`decl_notation`] with … with `ind_body` [`decl_notation`].
-                 : | Fixpoint `fix_body` [`decl_notation`] with … with `fix_body` [`decl_notation`].
-                 : | CoFixpoint `cofix_body` [`decl_notation`] with … with `cofix_body` [`decl_notation`].
-                 : | [Local] Declare Custom Entry `ident`.
+                 : [Local] Infix `string` := `qualid` [`modifiers`] [: `scope`].
+                 : [Local] Reserved Notation `string` [`modifiers`] .
+                 : Inductive `ind_body` [`decl_notation`] with … with `ind_body` [`decl_notation`].
+                 : CoInductive `ind_body` [`decl_notation`] with … with `ind_body` [`decl_notation`].
+                 : Fixpoint `fix_body` [`decl_notation`] with … with `fix_body` [`decl_notation`].
+                 : CoFixpoint `cofix_body` [`decl_notation`] with … with `cofix_body` [`decl_notation`].
+                 : [Local] Declare Custom Entry `ident`.
    decl_notation : [where `string` := `term` [: `scope`] and … and `string` := `term` [: `scope`]].
    modifiers     : at level `num`
                  : in custom `ident`
                  : in custom `ident` at level `num`
-                 : | `ident` , … , `ident` at level `num` [`binderinterp`]
-                 : | `ident` , … , `ident` at next level [`binderinterp`]
-                 : | `ident` `explicit_subentry`
-                 : | left associativity
-                 : | right associativity
-                 : | no associativity
-                 : | only parsing
-                 : | only printing
-                 : | format `string`
+                 : `ident` , … , `ident` at level `num` [`binderinterp`]
+                 : `ident` , … , `ident` at next level [`binderinterp`]
+                 : `ident` `explicit_subentry`
+                 : left associativity
+                 : right associativity
+                 : no associativity
+                 : only parsing
+                 : only printing
+                 : format `string`
    explicit_subentry : ident
-                 : | global
-                 : | bigint
-                 : | [strict] pattern [at level `num`]
-                 : | binder
-                 : | closed binder
-                 : | constr [`binderinterp`]
-                 : | constr at level `num` [`binderinterp`]
-                 : | constr at next level [`binderinterp`]
-                 : | custom [`binderinterp`]
-                 : | custom at level `num` [`binderinterp`]
-                 : | custom at next level [`binderinterp`]
+                 : global
+                 : bigint
+                 : [strict] pattern [at level `num`]
+                 : binder
+                 : closed binder
+                 : constr [`binderinterp`]
+                 : constr at level `num` [`binderinterp`]
+                 : constr at next level [`binderinterp`]
+                 : custom [`binderinterp`]
+                 : custom at level `num` [`binderinterp`]
+                 : custom at next level [`binderinterp`]
    binderinterp  : as ident
-                 : | as pattern
-                 : | as strict pattern
+                 : as pattern
+                 : as strict pattern
 
 .. note:: No typing of the denoted expression is performed at definition
           time. Type checking is done only at the time of use of the notation.
@@ -1692,13 +1692,13 @@ Tactic notations allow to customize the syntax of tactics. They have the followi
    tacn                 : Tactic Notation [`tactic_level`] [`prod_item` … `prod_item`] := `tactic`.
    prod_item            : `string` | `tactic_argument_type`(`ident`)
    tactic_level         : (at level `num`)
-   tactic_argument_type : ident | simple_intropattern | reference
-                        : | hyp | hyp_list | ne_hyp_list
-                        : | constr | uconstr | constr_list | ne_constr_list
-                        : | integer | integer_list | ne_integer_list
-                        : | int_or_var | int_or_var_list | ne_int_or_var_list
-                        : | tactic | tactic0 | tactic1 | tactic2 | tactic3
-                        : | tactic4 | tactic5
+   tactic_argument_type : `ident` | `simple_intropattern` | `reference`
+                        : `hyp` | `hyp_list` | `ne_hyp_list`
+                        : `constr` | `uconstr` | `constr_list` | `ne_constr_list`
+                        : `integer` | `integer_list` | `ne_integer_list`
+                        : `int_or_var` | `int_or_var_list` | `ne_int_or_var_list`
+                        : `tactic` | `tactic0` | `tactic1` | `tactic2` | `tactic3`
+                        : `tactic4` | `tactic5`
 
 .. cmd:: Tactic Notation {? (at level @level)} {+ @prod_item} := @tactic.