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.

1 files changed, 7 insertions, 9 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 31f3736bae..1dd68f2abf 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1642,15 +1642,13 @@ let drop_notations_pattern looked_for genv =
     | CPatCast (_,_) ->
       (* We raise an error if the pattern contains a cast, due to
          current restrictions on casts in patterns. Cast in patterns
-         are supported only in local binders and only at top
-         level. In fact, they are currently eliminated by the
-         parser. The only reason why they are in the
-         [cases_pattern_expr] type is that the parser needs to factor
-         the "(c : t)" notation with user defined notations (such as
-         the pair). In the long term, we will try to support such
-         casts everywhere, and use them to print the domains of
-         lambdas in the encoding of match in constr. This check is
-         here and not in the parser because it would require
+         are supported only in local binders and only at top level.
+         The only reason they are in the [cases_pattern_expr] type
+         is that the parser needs to factor the "c : t" notation
+         with user defined notations. In the long term, we will try to
+         support such casts everywhere, and perhaps use them to print
+         the domains of lambdas in the encoding of match in constr.
+         This check is here and not in the parser because it would require
          duplicating the levels of the [pattern] rule. *)
       CErrors.user_err ?loc ~hdr:"drop_notations_pattern"
                             (Pp.strbrk "Casts are not supported in this pattern.")