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 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/changelog/02-specification-language/10167-orpat-mixfix.rst b/doc/changelog/02-specification-language/10167-orpat-mixfix.rst index e3c3923348..2d17e569d3 100644 --- a/doc/changelog/02-specification-language/10167-orpat-mixfix.rst +++ b/doc/changelog/02-specification-language/10167-orpat-mixfix.rst @@ -7,6 +7,6 @@ + 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 + See :ref:`extendedpatternmatching` for details (`#10167 <https://github.com/coq/coq/pull/10167>`_, by Georges Gonthier). |