From f0df23f2c21fe837d72525388388a282d5aaef62 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 | 11 +++++++++++ 1 file changed, 11 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 0000000000000..a3ffaee6b5682 --- /dev/null +++ b/doc/changelog/11-standard-library/18500-deprecations_in_Numbers.rst @@ -0,0 +1,11 @@ +- **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).