Merge PR #9269: Move and rewrite intro pattern section

Ack-by: Zimmi48
Ack-by: anton-trunov
Ack-by: jfehrle

4 files changed, 51 insertions, 51 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.