Merge PR #10167: do not parse `|` as infix in patterns; parse `|}` as `|` `}`

Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: ggonthier
Reviewed-by: herbelin
Ack-by: jfehrle
Reviewed-by: mattam82

1 files changed, 11 insertions, 0 deletions

diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 5f0b63729b..9b381cb9de 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -925,6 +925,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
 ++++++++++++++++++++++++