From 4f4b9d04bc59dc1f3b6962b0b077ba274638efc7 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 13 Mar 2017 10:44:58 +0100
Subject: Document the changes to IZR.

---
 CHANGES | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/CHANGES b/CHANGES
index a7cba9aa4f..0acc2bb950 100644
--- a/CHANGES
+++ b/CHANGES
@@ -7,7 +7,7 @@ Tactics
   functional extensionality in H supposed to be a quantified equality
   until giving a bare equality.
 
-Libraries
+Standard Library
 
 - New file PropExtensionality.v to explicitly work in the axiomatic
   context of propositional extensionality.
@@ -16,6 +16,12 @@ Libraries
   Various proof-theoretic characterizations of choice over setoids in
   file ChoiceFacts.v.
 
+- IZR (Reals) has been changed to produce a compact representation of
+  integers. As a consequence, IZR is no longer convertible to INR and
+  lemmas such as INR_IZR_INZ should be used instead.
+- Real constants are now represented using IZR rather than R0 and R1;
+  this might cause rewriting rules to fail to apply to constants.
+
 Changes from V8.6beta1 to V8.6
 ==============================
 
-- 
cgit v1.2.3