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, 3 insertions, 2 deletions

diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 3a57c14a3b..5f982346ab 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -38,9 +38,9 @@ end
 
    - dynamic rules declared at the evaluation of Coq files (using
      e.g. Notation, Infix, or Tactic Notation)
-   - static rules explicitly defined in files g_*.ml4
+   - static rules explicitly defined in files g_*.mlg
    - static rules macro-generated by ARGUMENT EXTEND, TACTIC EXTEND and
-     VERNAC EXTEND (see e.g. file extratactics.ml4)
+     VERNAC EXTEND (see e.g. file extratactics.mlg)
 
    Note that parsing a Coq document is in essence stateful: the parser
    needs to recognize commands that start proofs and use a different
@@ -170,6 +170,7 @@ module Prim :
     val ne_string : string Entry.t
     val ne_lstring : lstring Entry.t
     val var : lident Entry.t
+    val bar_cbrace : unit Entry.t
   end
 
 module Constr :