Plus de piquants dans les actions des grammaires; nom de la grammaire pris comme parseur par defaut; le type List devient AstList

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

1 files changed, 6 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 9e29a7e50..f8cb0a410 100644
--- a/CHANGES
+++ b/CHANGES
@@ -16,3 +16,9 @@
 - Ajout de la syntaxe "[" phrase_1 ... phrase_n"]." pour grouper des
 phrases (utile pour Time et pour des grammaires abrégeant plusieurs
 commandes)
+
+- Le parseur par défaut des actions des règles de grammaires est
+maintenant celui associé au nom de la grammaire (vernac, tactic ou
+constr). Donc plus de piquants <:vernac:<...>> etc. Pour retourner de
+l'ast, il faut typer explicitement la grammaire avec Ast ou List
+(renommé d'ailleurs AstList).