MAJ

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

1 files changed, 9 insertions, 13 deletions

diff --git a/CHANGES b/CHANGES
index f773620b6c..167dd6528e 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,28 +1,24 @@
 Changes from V7.3.1 to V7.4
 ===========================
 
-Grammar extension
-
-- In old syntax, the only predefined non-terminal entries are ident,
-  global, constr and pattern (e.g. nvar, numarg disappears); the only
-  allowed grammar types are constr and pattern; ast and ast list are no
-  longer supported.
-- Some incompatibilities: precedence of product (cf FTA); when a
-  syntax is a initial segment of the other, Grammar does not work, use
-  Notation
-
 Symbolic notations
 
 - Introduction of a notion of scope gathering notations in a consistent set;
-  set a notation sets has been developped for nat, Z and R
+  a notation sets has been developped for nat, Z and R (undocumented)
 - New command "Notation" for declaring notations simultaneously for
-  parsing and printing
+  parsing and printing (see chap 10 of the reference manual)
 - Declarations with only implicit arguments now handled (e.g. the
   argument of nil can be set implicit; use !nil to refer to nil
   without arguments)
-- "Print Scope sc" and "Locate ntn" allows to know to what a notation is bound
+- "Print Scope sc" and "Locate ntn" allows to know to what expression a 
+  notation is bound
 - New defensive strategy for printing or not implicit arguments to ensure
   re-type-checkability of the printed term
+- In Grammar command, the only predefined non-terminal entries are ident,
+  global, constr and pattern (e.g. nvar, numarg disappears); the only
+  allowed grammar types are constr and pattern; ast and ast list are no
+  longer supported; some incompatibilities in Grammar: when a syntax is a 
+  initial segment of an other one,  Grammar does not work, use Notation
 
 Library