From 5a38fdb4af87f66632d036848e370948ead50c50 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 3 Feb 2004 17:36:04 +0000
Subject: MAJ

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

diff --git a/CHANGES b/CHANGES
index 869cc9a084..6d21026ac4 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
 ============================================
-- 
cgit v1.2.3