do not parse `|` as infix in patterns; parse `|}` as `|` `}`

* use mixfix `(p1 | … | pn)` notation for nested disjunctive patterns,
rather than infix `|`, making pattern syntax consistent with term
syntax.
* disable extending `pattern` grammar with notation incompatible with
the nested disjunctive pattern syntax `(p1 | … | pn)`, such as the `(p
| q)` divisibility notation used by `Numbers`.
* emit a (disabled by default) `disj-pattern-notation` warning when such
`Notation` is attempted.
* update documentation accordingly; document incompatibilities in
`changelog`.
* comment special treatment of `(num)` in grammar.
* update file extensions in `Pcoq` header comment.
* correct the keyword declarations to reflect the contents of the
grammar files; perhaps there should be an option to disable implicit
keyword extension in a `.mlg` file, so that these lists could actually
be checked.
* parse the `|}` manifest record terminator as `|` followed by `}`,
eliminating the `|}` token which conflicts with notations that use `|`
as a terminator (such as, absolute value, norm, or cardinal in
MathComp). Since `|` is now an `operconstr` _and_ `pattern` terminator,
`bar_cbrace` rule checks for contiguous symbols, this change entails no
visible behaviour change.

4 files changed, 28 insertions, 5 deletions

diff --git a/doc/changelog/02-specification-language/10167-orpat-mixfix.rst b/doc/changelog/02-specification-language/10167-orpat-mixfix.rst
new file mode 100644
index 0000000000..e3c3923348
--- /dev/null
+++ b/doc/changelog/02-specification-language/10167-orpat-mixfix.rst
@@ -0,0 +1,12 @@
+- Require parentheses around nested disjunctive patterns, so that pattern and
+  term syntax are consistent; match branch patterns no longer require
+  parentheses for notation at level 100 or more. Incompatibilities:
+
+  + in :g:`match p with (_, (0|1)) => ...` parentheses may no longer be
+    omitted around :n:`0|1`.
+  + notation :g:`(p | q)` now potentially clashes with core pattern syntax,
+    and should be avoided. ``-w disj-pattern-notation`` flags such :cmd:`Notation`.
+
+  see :ref:`extendedpatternmatching` for details
+  (`#10167 <https://github.com/coq/coq/pull/10167>`_,
+  by Georges Gonthier).
diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst
index e882ce6e88..b568160356 100644
--- a/doc/sphinx/addendum/extended-pattern-matching.rst
+++ b/doc/sphinx/addendum/extended-pattern-matching.rst
@@ -21,10 +21,10 @@ type is considered to be a variable. A variable name cannot occur more
 than once in a given pattern. It is recommended to start variable
 names by a lowercase letter.
 
-If a pattern has the form ``(c x)`` where ``c`` is a constructor symbol and x
+If a pattern has the form ``c x`` where ``c`` is a constructor symbol and x
 is a linear vector of (distinct) variables, it is called *simple*: it
 is the kind of pattern recognized by the basic version of match. On
-the opposite, if it is a variable ``x`` or has the form ``(c p)`` with ``p`` not
+the opposite, if it is a variable ``x`` or has the form ``c p`` with ``p`` not
 only made of variables, the pattern is called *nested*.
 
 A variable pattern matches any value, and the identifier is bound to
@@ -216,7 +216,8 @@ Here is an example:
      end.
 
 
-Here is another example using disjunctive subpatterns.
+Nested disjunctive patterns are allowed, inside parentheses, with the
+notation :n:`({+| @pattern})`, as in:
 
 .. coqtop:: in
 
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 8acbcbec8f..ebaa6fde66 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -185,8 +185,7 @@ is described in Chapter :ref:`syntaxextensionsandinterpretationscopes`.
                     : `qualid`
                     : _
                     : `num`
-                    : ( `or_pattern` , … , `or_pattern` )
-   or_pattern       : `pattern` | … | `pattern`
+                    : ( `pattern` | … | `pattern` )
 
 
 Types
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 3710c0af9d..aee5f66bb6 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -924,6 +924,17 @@ notations are given below. The optional :production:`scope` is described in
           given to some notation, say ``"{ y } & { z }"`` in fact applies to the
           underlying ``"{ x }"``\-free rule which is ``"y & z"``).
 
+.. note:: Notations such as ``"( p | q )"`` (or starting with ``"( x | "``,
+          more generally) are deprecated as they conflict with the syntax for
+          nested disjunctive patterns (see :ref:`extendedpatternmatching`),
+          and are not honored in pattern expressions.
+
+          .. warn:: Use of @string Notation is deprecated as it is inconsistent with pattern syntax.
+
+             This warning is disabled by default to avoid spurious diagnostics
+             due to legacy notation in the Coq standard library.
+             It can be turned on with the ``-w disj-pattern-notation`` flag.
+
 Persistence of notations
 ++++++++++++++++++++++++