Nouveau déplacement de constr, cette fois au niveau 8. En fait, il y a

un problème dû à la non réversibilité de la suppression de règles
camlp4 vis à vis de l'insertion : lorsqu'un niveau existant vide est
étendu, la suppression non seulement efface l'extension mais aussi le
niveau lui-même. Ceci a un effet sur les niveaux vides 8 et 99. Nous
n'avons pas trouvé de bonne solution à ce problème et l'utilisation
d'extensions aux niveaux 99 ou 8 (anciennement 5 avant ce commit)
continue de corrompre le parser si effectuées à l'intérieur de section
ou de modules. Voici un exemple montrant le problème :

Print Grammar constr. (* le niveau "8" existe *)
Section A.
Notation "{{ x }}" := (S x) (at level 8).
End A.
Print Grammar constr. (* le niveau "8" n'existe plus *)
Goal True. 
apply I.  (* appelle le niveau constr qui continue d'appeler "8"... échec *)



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

1 files changed, 1 insertions, 2 deletions

diff --git a/CHANGES b/CHANGES
index 8c9a2e7bdf..7a54ecf615 100644
--- a/CHANGES
+++ b/CHANGES
@@ -8,8 +8,7 @@ Commands
 
 Notations
 
-- Level "constr" moved from 9 to 5. User notations from levels 6 to 9
-  may have to be put at levels below 5 to be used without parentheses.
+- Level "constr" moved from 9 to 8.
 
 Tactic Language