From 7030dc49d4ddc107d131b2f199a5002a5d8e432e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 12 Oct 2001 09:36:29 +0000
Subject: MAJ

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2111 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 CHANGES | 10 ++++++++++
 1 file changed, 10 insertions(+)

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
-- 
cgit v1.2.3