diff options
| author | Anton Trunov | 2020-05-12 18:29:28 +0300 |
|---|---|---|
| committer | Anton Trunov | 2020-05-12 18:29:28 +0300 |
| commit | 5784bb98aaa3e4eab4cd3e9871afb4b40d82f62c (patch) | |
| tree | bbe30c8c8aaffbd387e886bae4c017db9c525b90 /doc | |
| parent | efb78e3c413bcc66d470ba4046c56bae0a61f56f (diff) | |
| parent | 1019cb48c80260d7df27096826e8594ec242dc5a (diff) | |
Merge PR #12162: Fixing #12161: rename Bool.leb into Bool.le
Ack-by: Zimmi48
Reviewed-by: anton-trunov
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/10-standard-library/12008-ollibs-bool.rst | 2 | ||||
| -rw-r--r-- | doc/changelog/10-standard-library/12162-bool-leb.rst | 4 |
2 files changed, 5 insertions, 1 deletions
diff --git a/doc/changelog/10-standard-library/12008-ollibs-bool.rst b/doc/changelog/10-standard-library/12008-ollibs-bool.rst index 7c10d261a7..42e5eb96eb 100644 --- a/doc/changelog/10-standard-library/12008-ollibs-bool.rst +++ b/doc/changelog/10-standard-library/12008-ollibs-bool.rst @@ -1,5 +1,5 @@ - **Added:** - Order relations ``ltb`` and ``compareb`` added in ``Bool.Bool``. + Order relations ``lt`` and ``compare`` added in ``Bool.Bool``. Order properties for ``bool`` added in ``Bool.BoolOrder`` as well as two modules ``Bool_as_OT`` and ``Bool_as_DT`` in ``Structures.OrdersEx`` (`#12008 <https://github.com/coq/coq/pull/12008>`_, by Olivier Laurent). diff --git a/doc/changelog/10-standard-library/12162-bool-leb.rst b/doc/changelog/10-standard-library/12162-bool-leb.rst new file mode 100644 index 0000000000..6a4070a82e --- /dev/null +++ b/doc/changelog/10-standard-library/12162-bool-leb.rst @@ -0,0 +1,4 @@ +- **Deprecated:** + ``Bool.leb`` in favor of ``Bool.le``. The definition of ``Bool.le`` is made local to avoid conflicts with ``Nat.le``. As a consequence, previous calls to ``leb`` based on importing ``Bool`` should now be qualified into ``Bool.le`` even if ``Bool`` is imported. + (`#12162 <https://github.com/coq/coq/pull/12162>`_, + by Olivier Laurent). |