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, 4 insertions, 1 deletions

diff --git a/test-suite/success/Case18.v b/test-suite/success/Case18.v
index be9ca8d41b..6bea435090 100644
--- a/test-suite/success/Case18.v
+++ b/test-suite/success/Case18.v
@@ -1,7 +1,10 @@
 (* Check or-patterns *)
 
+(* Non-interference with Numbers divisibility. *)
+Reserved Notation "( p | q )" (at level 0).
+
 Definition g x :=
-  match x with ((((1 as x),_) | (_,x)), (_,(2 as y))|(y,_)) => (x,y) end.
+  match x with ((((1 as x),_) | (_,x)), ((_,(2 as y)) | (y,_))) => (x,y) end.
 
 Check (refl_equal _ : g ((1,2),(3,4)) = (1,3)).