diff options
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 35 |
1 files changed, 35 insertions, 0 deletions
@@ -6,6 +6,41 @@ Tactics - New tactic "extensionality in H" which applies (possibly dependent) functional extensionality in H supposed to be a quantified equality until giving a bare equality. +- New representation of terms that statically ensure stability by + evar-expansion. This has several consequences. + * In terms of performance, this adds a cost to every term destructuration, + but at the same time most eager evar normalizations were removed, which + couterbalances this drawback and even sometimes outperforms the old + implementation. For instance, many operations that would require O(n) + normalization of the term are now O(1) in tactics. YMMV. + * This triggers small changes in unification, which was not evar-insensitive. + Most notably, the new implementation recognizes Miller patterns that were + missed before because of a missing normalization step. Hopefully this should + be fairly uncommon. +- "auto with real" can now discharge comparisons of literals + +Standard Library + +- New file PropExtensionality.v to explicitly work in the axiomatic + context of propositional extensionality. +- New file SetoidChoice.v axiomatically providing choice over setoids, + and, consequently, choice of representatives in equivalence classes. + 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. + +Plugins + +- The mathematical proof language (also known as declarative mode) was removed. + +Dependencies + +- Support for camlp4 has been removed. Changes from V8.6beta1 to V8.6 ============================== |