blob: 87e4c9ff100f044f7ebd064f3925e4b19822532b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
- **Changed:**
Require parentheses around nested disjunctive patterns, so that pattern and
term syntax are consistent; match branch patterns no longer require
parentheses for notation at level 100 or more.
.. warning:: Incompatibilities
+ In :g:`match p with (_, (0|1)) => ...` parentheses may no longer be
omitted around :n:`0|1`.
+ Notation :g:`(p | q)` now potentially clashes with core pattern syntax,
and should be avoided. ``-w disj-pattern-notation`` flags such :cmd:`Notation`.
See :ref:`extendedpatternmatching` for details
(`#10167 <https://github.com/coq/coq/pull/10167>`_,
by Georges Gonthier).
|
