MAJ

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

1 files changed, 10 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 4577ae5035..0452542024 100644
--- a/CHANGES
+++ b/CHANGES
@@ -6,6 +6,16 @@ Tactics
 - New tactic "ClearBody H" to clear the body of definitions in local context
 - New tactic "Assert H := c" for forward reasoning
 
+Efficiency
+
+- Improved efficiency wrt .vo sizes and compilation times
+
+Bugs
+
+- Apply "universe anomaly" bug fixed
+- Bug with recursive inductive types involving let-in fixed
+- Confusion between implicit args of locals and globals of same base name fixed
+- NatRing works (to check)
 
 ----------------------------------------------------------------------------
 Changes from V6.3.1 and V7.0 to V7.1