Remontée de constr de 1 à 5 (pour permettre des notations entre 1 et 5

tout en évitant que les .. soient dans constr)


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

1 files changed, 7 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index ed69d91040..8c9a2e7bdf 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,9 +1,16 @@
 Changes from V8.1gamma to ...
 =============================
 
+Commands
+
 - Added option Global to "Implicit Arguments" and "Arguments Scope" for
   section surviving.
 
+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.
+
 Tactic Language
 
 - Second-order pattern-matching now working in Ltac "match" clauses