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 +++++++
 parsing/g_constr.ml4 | 3 ++-
 parsing/pcoq.ml4     | 1 +
 3 files changed, 10 insertions(+), 1 deletion(-)

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
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index bdea94a048..f2316ec5e1 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -131,7 +131,7 @@ GEXTEND Gram
     [ [ c = operconstr LEVEL "200" -> c ] ]
   ;
   constr:
-    [ [ c = operconstr LEVEL "1" -> c ] ]
+    [ [ c = operconstr LEVEL "5" -> c ] ]
   ;
   operconstr:
     [ "200" RIGHTA
@@ -160,6 +160,7 @@ GEXTEND Gram
     | "9"
         [ ".."; c = operconstr LEVEL "0"; ".." ->
           CAppExpl (loc,(None,Ident (loc,Topconstr.ldots_var)),[c]) ]
+    | "5" LEFTA [ ]
     | "1" LEFTA
       [ c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" ->
 	CApp(loc,(Some (List.length args+1),CRef f),args@[c,None])
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index ecbc2ef6c0..8f23c0f30e 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -487,6 +487,7 @@ let default_levels =
    90,Gramext.RightA;
    10,Gramext.RightA;
    9,Gramext.RightA;
+   5,Gramext.LeftA;
    1,Gramext.LeftA;
    0,Gramext.RightA]
 
-- 
cgit v1.2.3