diff options
| author | Hugo Herbelin | 2020-03-26 08:45:43 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-03-26 08:45:43 +0100 |
| commit | 84f6394f78baea5b1f261765164ae23cd245a357 (patch) | |
| tree | d7a0b4da8708f5f261f66c8ccd6ed1c48cafd988 /doc | |
| parent | 1217583de0c7ac0d17c8917f21c30c247176d83f (diff) | |
| parent | 528dd28a48dd7b1898212e2aae9b43bb19fb91cc (diff) | |
Merge PR #11891: Fix levels of `<=?` and `<?` in the stdlib
Reviewed-by: herbelin
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/10-standard-library/11891-fix-order-notations.rst | 10 |
1 files changed, 10 insertions, 0 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 new file mode 100644 index 0000000000..d58d26244a --- /dev/null +++ b/doc/changelog/10-standard-library/11891-fix-order-notations.rst @@ -0,0 +1,10 @@ +- **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). |