aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
Diffstat (limited to 'doc')
-rw-r--r--doc/changelog/10-standard-library/12008-ollibs-bool.rst5
-rw-r--r--doc/stdlib/index-list.html.template1
2 files changed, 6 insertions, 0 deletions
diff --git a/doc/changelog/10-standard-library/12008-ollibs-bool.rst b/doc/changelog/10-standard-library/12008-ollibs-bool.rst
new file mode 100644
index 0000000000..7c10d261a7
--- /dev/null
+++ b/doc/changelog/10-standard-library/12008-ollibs-bool.rst
@@ -0,0 +1,5 @@
+- **Added:**
+ Order relations ``ltb`` and ``compareb`` 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/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index b2c9c936c9..4a62888552 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -99,6 +99,7 @@ through the <tt>Require Import</tt> command.</p>
<dd>
theories/Bool/Bool.v
theories/Bool/BoolEq.v
+ theories/Bool/BoolOrder.v
theories/Bool/DecBool.v
theories/Bool/IfProp.v
theories/Bool/Sumbool.v