Merge PR #6599: Decimals in prelude

1 files changed, 9 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 7ea23eeb7..2040c1b57 100644
--- a/CHANGES
+++ b/CHANGES
@@ -99,6 +99,15 @@ Documentation
   moved to the GitHub wiki section of this repository; the main entry
   page is https://github.com/coq/coq/wiki/The-Coq-FAQ.
 
+Standard Library
+
+- New libraries Coq.Init.Decimal, Coq.Numbers.DecimalFacts,
+  Coq.Numbers.DecimalNat, Coq.Numbers.DecimalPos,
+  Coq.Numbers.DecimalN, Coq.Numbers.DecimalZ,
+  Coq.Numbers.DecimalString providing a type of decimal numbers, some
+  facts about them, and conversions between decimal numbers and nat,
+  positive, N, Z, and string.
+
 Changes from 8.7.1 to 8.7.2
 ===========================