Merge PR #9269: Move and rewrite intro pattern section

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

3 files changed, 83 insertions, 83 deletions

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