aboutsummaryrefslogtreecommitdiff
path: root/parsing
diff options
context:
space:
mode:
authorHugo Herbelin2017-11-26 19:18:38 +0100
committerHugo Herbelin2017-11-27 11:27:34 +0100
commit134b220b77d74b0ada801d215a2e5c66bc6726ea (patch)
tree27889d694009730a3fd0db51587b95c725fa26c4 /parsing
parentc1e670b386f83ed78104a6eb6e4d17cc1d906439 (diff)
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).
Diffstat (limited to 'parsing')
-rw-r--r--parsing/egramcoq.ml4
-rw-r--r--parsing/g_constr.ml42
2 files changed, 3 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)