MAJ

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

1 files changed, 9 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 869cc9a08..6d21026ac 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,6 +1,12 @@
 Changes from V8.0beta to V8.0
 =============================
 
+Commands
+
+- New option "Set Printing All" to deactivate all high-level forms of
+  printing (implicit arguments, coercions, destructing let,
+  if-then-else, notations, projections)
+
 Syntax
 
 - Command "Print." discontinued.
@@ -17,6 +23,9 @@ Bug fixes
 - Translator printing bug of reals fixed
 - Fix bugs in induction/destruct in case the type of the eliminated object 
   has parameters
+- Fix a printing bug with lambda-variable names inherited from the names of 
+  a product cast
+- Fix a bug with Focus
 
 Changes from V8.0beta old syntax to V8.0beta
 ============================================