diff options
Diffstat (limited to 'doc/changelog/10-standard-library/11891-fix-order-notations.rst')
| -rw-r--r-- | doc/changelog/10-standard-library/11891-fix-order-notations.rst | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/doc/changelog/10-standard-library/11891-fix-order-notations.rst b/doc/changelog/10-standard-library/11891-fix-order-notations.rst deleted file mode 100644 index d58d26244a..0000000000 --- a/doc/changelog/10-standard-library/11891-fix-order-notations.rst +++ /dev/null @@ -1,10 +0,0 @@ -- **Changed:** - Notations :g:`<=?` and :g:`<?` from ``Coq.Structures.Orders`` and - ``Coq.Sorting.Mergesort.NatOrder`` are now at level 70 rather than - 35, so as to be compatible with the notations defined everywhere - else in the standard library. This may require re-parenthesizing - some expressions. These notations were breaking the ability to - import modules from the standard library that were otherwise - compatible (fixes `#11890 - <https://github.com/coq/coq/issues/11890>`_, `#11891 - <https://github.com/coq/coq/pull/11891>`_, by Jason Gross). |