Add changelog entry for coq#18500

Villetaneuse · Jan 19, 2024 · c4c78db · c4c78db
1 parent 49680bc
commit c4c78db
Showing 1 changed file with 13 additions and 0 deletions.
diff --git a/doc/changelog/11-standard-library/18500-deprecations_in_Numbers.rst b/doc/changelog/11-standard-library/18500-deprecations_in_Numbers.rst
@@ -0,0 +1,13 @@
+- **Deprecated:**
+  The library files
+
+  * ``Coq.Numbers.Integer.Binary.ZBinary``
+  * ``Coq.Numbers.Integer.NatPairs.ZNatPairs``
+  * ``Coq.Numbers.Natural.Binary.NBinary``
+
+  have been deprecated.
+  Users should require ``Coq.Arith.PeanoNat`` or ``Coq.Arith.NArith.BinNat``
+  if they want implementations of natural numbers and
+  ``Coq.Arith.ZArith.BinInt`` if they want an implementation of integers.
+  (`#18500 <https://github.com/coq/coq/pull/18500>`_,
+  by Pierre Rousselin).