diff --git a/doc/changelog/11-standard-library/18500-deprecations_in_Numbers.rst b/doc/changelog/11-standard-library/18500-deprecations_in_Numbers.rst new file mode 100644 index 000000000000..f513599dc843 --- /dev/null +++ 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 `_, + by Pierre Rousselin).