aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2020-06-19 21:16:19 +0200
committerEmilio Jesus Gallego Arias2020-08-27 19:03:33 +0200
commit21dd85bf7aa8c16e15735f5946650a200c9566f5 (patch)
tree88f21220eaf352870bfcf4068e33d5f3dbeba70c /doc
parent5a28133182c75292d9b2adc7826cba47e6a138a7 (diff)
[zarith] Changelog
Diffstat (limited to 'doc')
-rw-r--r--doc/changelog/11-infrastructure-and-dependencies/11742-zarith+core.rst8
1 files changed, 8 insertions, 0 deletions
diff --git a/doc/changelog/11-infrastructure-and-dependencies/11742-zarith+core.rst b/doc/changelog/11-infrastructure-and-dependencies/11742-zarith+core.rst
new file mode 100644
index 0000000000..3b34e11ff8
--- /dev/null
+++ b/doc/changelog/11-infrastructure-and-dependencies/11742-zarith+core.rst
@@ -0,0 +1,8 @@
+- **Changed:**
+ Coq's core system now uses the `zarith <https://github.com/ocaml/Zarith>`_
+ library, based on GNU's gmp instead of ``num`` which is
+ deprecated upstream. The custom ``bigint`` module is
+ not longer provided; note that the ``micromega`` still uses
+ ``num``
+ (`#11742 <https://github.com/coq/coq/pull/11742>`_,
+ by Emilio Jesus Gallego Arias and Vicent Laporte).