From 134b220b77d74b0ada801d215a2e5c66bc6726ea Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 26 Nov 2017 19:18:38 +0100
Subject: Fixing associativity registered for level 10.

Apparently a long-standing bug, coupled with a pattern/constr
associativity inconsistency introduced while fixing another
pattern/constr level inconsistency (bug #4272, 0917ce7c).
---
 parsing/egramcoq.ml            | 4 ++--
 parsing/g_constr.ml4           | 2 +-
 test-suite/success/Notations.v | 6 ++++++
 3 files changed, 9 insertions(+), 3 deletions(-)

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 2cb7da5694..acbe2d982d 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -35,7 +35,7 @@ let default_levels =
    100,Extend.RightA,false;
    99,Extend.RightA,true;
    90,Extend.RightA,true;
-   10,Extend.RightA,false;
+   10,Extend.LeftA,false;
    9,Extend.RightA,false;
    8,Extend.RightA,true;
    1,Extend.LeftA,false;
@@ -47,7 +47,7 @@ let default_pattern_levels =
    99,Extend.RightA,true;
    90,Extend.RightA,true;
    11,Extend.LeftA,false;
-   10,Extend.RightA,false;
+   10,Extend.LeftA,false;
    1,Extend.LeftA,false;
    0,Extend.RightA,false]
 
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 844c040fdf..bfebca2a5c 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -380,7 +380,7 @@ GEXTEND Gram
     | "11" LEFTA
       [ p = pattern; "as"; id = ident ->
         CAst.make ~loc:!@loc @@ CPatAlias (p, id) ]
-    | "10" RIGHTA
+    | "10" LEFTA
       [ p = pattern; lp = LIST1 NEXT ->
         (let open CAst in match p with
 	  | { v = CPatAtom (Some r) } -> CAst.make ~loc:!@loc @@ CPatCstr (r, None, lp)
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index e3f90f6d94..3c0ad20700 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -147,3 +147,9 @@ Inductive EQ {A} (x:A) : A -> Prop := REFL : x === x
 
 Fail Check {x@{u},y|x=x}.
 Fail Check {?[n],y|0=0}.
+
+(* Check that 10 is well declared left associative *)
+
+Section C.
+Notation "f $$$ x" := (id f x) (at level 10, left associativity).
+End C.
-- 
cgit v1.2.3


From 257e14b19e9026a4f3cdfa991e27293faf110324 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 26 Nov 2017 19:33:00 +0100
Subject: Releasing level "11" of "pattern".

Was introduced in 0917ce7c to fix #4272, but it seems that we can fix
it by just merging levels 10 and 11. This prevents the worry of fixing
the associativity of level 11 to left in 0917ce7c.
---
 parsing/egramcoq.ml  | 1 -
 parsing/g_constr.ml4 | 7 +++----
 2 files changed, 3 insertions(+), 5 deletions(-)

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index acbe2d982d..9c2766187e 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -46,7 +46,6 @@ let default_pattern_levels =
    100,Extend.RightA,false;
    99,Extend.RightA,true;
    90,Extend.RightA,true;
-   11,Extend.LeftA,false;
    10,Extend.LeftA,false;
    1,Extend.LeftA,false;
    0,Extend.RightA,false]
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index bfebca2a5c..6af8f0b9e1 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -377,11 +377,10 @@ GEXTEND Gram
       [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> CAst.make ~loc:!@loc @@ CPatOr (p::pl) ]
     | "99" RIGHTA [ ]
     | "90" RIGHTA [ ]
-    | "11" LEFTA
-      [ p = pattern; "as"; id = ident ->
-        CAst.make ~loc:!@loc @@ CPatAlias (p, id) ]
     | "10" LEFTA
-      [ p = pattern; lp = LIST1 NEXT ->
+      [ p = pattern; "as"; id = ident ->
+        CAst.make ~loc:!@loc @@ CPatAlias (p, id)
+      | p = pattern; lp = LIST1 NEXT ->
         (let open CAst in match p with
 	  | { v = CPatAtom (Some r) } -> CAst.make ~loc:!@loc @@ CPatCstr (r, None, lp)
 	  | { v = CPatCstr (r, None, l2); loc } ->
-- 
cgit v1.2.3


From 7d0eb42050cb4f75c95cefb11c0cac5efa32f40a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 26 Nov 2017 19:34:14 +0100
Subject: A cosmetic standardization: adding a space in g_constr.ml4.

---
 parsing/g_constr.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 6af8f0b9e1..7e5933cea2 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -391,7 +391,7 @@ GEXTEND Gram
           | _ -> CErrors.user_err
                  ?loc:(cases_pattern_expr_loc p) ~hdr:"compound_pattern"
                  (Pp.str "Such pattern cannot have arguments."))
-      |"@"; r = Prim.reference; lp = LIST0 NEXT ->
+      | "@"; r = Prim.reference; lp = LIST0 NEXT ->
         CAst.make ~loc:!@loc @@ CPatCstr (r, Some lp, []) ]
     | "1" LEFTA
       [ c = pattern; "%"; key=IDENT -> CAst.make ~loc:!@loc @@ CPatDelimiters (key,c) ]
-- 
cgit v1.2.3