From 0917ce7cf48cadacc6fca48ba18b395740cccbe2 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 1 Jul 2015 11:25:47 +0200
Subject: Notation: use same level for "@" in constr: and pattern: (Close:
 #4272)

A possible script breakage can occur if one has a notation
at level 11 that is also right associative (now 11 is left associative).

Thanks Georges for debugging that.
---
 parsing/g_constr.ml4          |  4 ++--
 parsing/pcoq.ml4              |  4 ++--
 test-suite/bugs/closed/4272.v | 12 ++++++++++++
 3 files changed, 16 insertions(+), 4 deletions(-)
 create mode 100644 test-suite/bugs/closed/4272.v

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 74f17f9fb6..e47e3fb1e6 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -364,10 +364,10 @@ GEXTEND Gram
     | "100" RIGHTA
       [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> CPatOr (!@loc,p::pl) ]
     | "99" RIGHTA [ ]
-    | "10" LEFTA
+    | "11" LEFTA
       [ p = pattern; "as"; id = ident ->
 	  CPatAlias (!@loc, p, id) ]
-    | "9" RIGHTA
+    | "10" RIGHTA
       [ p = pattern; lp = LIST1 NEXT ->
         (match p with
 	  | CPatAtom (_, Some r) -> CPatCstr (!@loc, r, [], lp)
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 54edbb2c88..797b031fe4 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -459,8 +459,8 @@ let default_pattern_levels =
   [200,Extend.RightA,true;
    100,Extend.RightA,false;
    99,Extend.RightA,true;
-   10,Extend.LeftA,false;
-   9,Extend.RightA,false;
+   11,Extend.LeftA,false;
+   10,Extend.RightA,false;
    1,Extend.LeftA,false;
    0,Extend.RightA,false]
 
diff --git a/test-suite/bugs/closed/4272.v b/test-suite/bugs/closed/4272.v
new file mode 100644
index 0000000000..aeb4c9bb95
--- /dev/null
+++ b/test-suite/bugs/closed/4272.v
@@ -0,0 +1,12 @@
+Set Implicit Arguments.
+
+Record foo := Foo { p1 : Type; p2 : p1 }.
+
+Variable x : foo.
+
+Let p := match x with @Foo a b => a end.
+
+Notation "@ 'id'"  := 3 (at level 10).
+Notation "@ 'sval'" := 3 (at level 10).
+
+Let q := match x with @Foo a b => a end.
-- 
cgit v1.2.3