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

diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 568e5b9997..9bc225475d 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -546,6 +546,15 @@ let extend_constr state forpat ng =
 
 let constr_levels = GramState.field ()
 
+let is_disjunctive_pattern_rule ng =
+  String.is_sub "( _ | " (snd ng.notgram_notation) 0
+
+let warn_disj_pattern_notation =
+  let open Pp in
+  let pp ng = str "Use of " ++ Notation.pr_notation ng.notgram_notation ++
+              str " Notation is deprecated as it is inconsistent with pattern syntax." in
+  CWarnings.create ~name:"disj-pattern-notation" ~category:"notation" ~default:CWarnings.Disabled pp
+
 let extend_constr_notation ng state =
   let levels = match GramState.get state constr_levels with
   | None -> String.Map.add "constr" default_constr_levels String.Map.empty
@@ -553,8 +562,13 @@ let extend_constr_notation ng state =
   in
   (* Add the notation in constr *)
   let (r, levels) = extend_constr levels ForConstr ng in
-  (* Add the notation in cases_pattern *)
-  let (r', levels) = extend_constr levels ForPattern ng in
+  (* Add the notation in cases_pattern, unless it would disrupt *)
+  (* parsing nested disjunctive patterns. *)
+  let (r', levels) =
+    if is_disjunctive_pattern_rule ng then begin
+       warn_disj_pattern_notation ng;
+       ([], levels)
+    end else extend_constr levels ForPattern ng in
   let state = GramState.set state constr_levels levels in
   (r @ r', state)