- Correction d'un bug de make_clenv_binding_apply révélé par le commit 9771

  (les let-in étaient comptés comme des produits, introduisant une incohérence
  sur le nombre de produits à instancier dans les lemmes appelés par apply).
- Export simplest_eapply pour utilisation dans Sophia/RecursiveDefinition.
- Doc développeur



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9785 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 10 insertions, 4 deletions

diff --git a/CHANGES b/CHANGES
index aa8a59413..9db0cec4e 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,13 +1,18 @@
-Changes from V8.1gamma to ...
-=============================
+Changes from V8.1 to V8.2
+=========================
 
 Commands
 
 - Added option Global to "Implicit Arguments" and "Arguments Scope" for
   section surviving.
-
 - Added option "Unset Elimination Schemes" to deactivated the automatic
-generation of elimination schemes.
+  generation of elimination schemes.
+
+Libraries
+
+- Better computational behavior of some constants (eq_nat_dec more
+  efficient, Z_lt_le_dec transparent, ...) [exceptionally source of
+  incompatibilities].
 
 Notations
 
@@ -31,6 +36,7 @@ Tactics
   ident], [apply <- term in ident] for applying equivalences (iff).
 - Slight improvement of the hnf and simpl tactics when applied on
   expressions with explicit occurrences of match or fix.
+- Better heuristic of lemma unfolding for apply/eapply.
 
 Changes from V8.1gamma to V8.1
 ==============================