diff options
Diffstat (limited to 'doc/changelog/02-specification-language/10167-orpat-mixfix.rst')
| -rw-r--r-- | doc/changelog/02-specification-language/10167-orpat-mixfix.rst | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/doc/changelog/02-specification-language/10167-orpat-mixfix.rst b/doc/changelog/02-specification-language/10167-orpat-mixfix.rst new file mode 100644 index 0000000000..e3c3923348 --- /dev/null +++ b/doc/changelog/02-specification-language/10167-orpat-mixfix.rst @@ -0,0 +1,12 @@ +- 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. 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). |