Réforme de l'interprétation des termes :

- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t"
- "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième
  pretty-printer dans ppconstr.ml est basé sur "constr_expr".
- Nouveau répertoire "interp" qui hérite de la partie interprétation qui
  se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml;
  constrextern.ml est l'équivalent de termast.ml pour le nouveau
  printer; topconstr.ml; contient la définition de "constr_expr";
  modintern.ml remplace astmod.ml)
- Libnames.reference tend à remplacer Libnames.qualid


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

1 files changed, 7 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 0900445c97..5be095ab8e 100644
--- a/CHANGES
+++ b/CHANGES
@@ -3,6 +3,13 @@ Changes from V7.3.1 to ????
 
 TODO: unification 2eme ordre avec NewDestruct
 
+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.
+
 Symbolic notations
 
 - Introduction of a notion of scope gathering notations in a consistent set;