aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
Diffstat (limited to 'doc')
-rw-r--r--doc/changelog/10-standard-library/09811-remove-zlogarithm.rst3
-rw-r--r--doc/stdlib/index-list.html.template1
2 files changed, 3 insertions, 1 deletions
diff --git a/doc/changelog/10-standard-library/09811-remove-zlogarithm.rst b/doc/changelog/10-standard-library/09811-remove-zlogarithm.rst
new file mode 100644
index 0000000000..3533764964
--- /dev/null
+++ b/doc/changelog/10-standard-library/09811-remove-zlogarithm.rst
@@ -0,0 +1,3 @@
+- Removes deprecated module `Coq.ZArith.Zlogarithm`
+ (#9881 <https://github.com/coq/coq/pull/9811>
+ by Vincent Laporte).
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index a561de1d0c..8d481b7f03 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -188,7 +188,6 @@ through the <tt>Require Import</tt> command.</p>
theories/ZArith/Zdiv.v
theories/ZArith/Zquot.v
theories/ZArith/Zeuclid.v
- theories/ZArith/Zlogarithm.v
(theories/ZArith/ZArith.v)
theories/ZArith/Zgcd_alt.v
theories/ZArith/Zwf.v