aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2017-03-13 10:44:58 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-03-22 18:13:16 +0100
commit4f4b9d04bc59dc1f3b6962b0b077ba274638efc7 (patch)
tree7634bfcb05fc4053a7ccd290d9b1bb19ef5d5520 /CHANGES
parent4e6fa17a3ef0b8d12cb8d55305f302338589ad1c (diff)
Document the changes to IZR.
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES8
1 files changed, 7 insertions, 1 deletions
diff --git a/CHANGES b/CHANGES
index a7cba9aa4..0acc2bb95 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
==============================