From c4c78db2b8429a39c401cd8df5ec6c350b79cf46 Mon Sep 17 00:00:00 2001 From: Pierre Rousselin Date: Fri, 19 Jan 2024 08:53:01 +0100 Subject: [PATCH] Add changelog entry for #18500 --- .../18500-deprecations_in_Numbers.rst | 13 +++++++++++++ 1 file changed, 13 insertions(+) create mode 100644 doc/changelog/11-standard-library/18500-deprecations_in_Numbers.rst 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).