From 8aa6ed2d10ddefb348f98684e691e25e4866b6ca Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 10 Apr 2007 16:36:36 +0000
Subject: 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
---
 CHANGES | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'CHANGES')

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
-- 
cgit v1.2.3