aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-10-03 15:05:44 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-10-03 15:05:44 +0200
commit3af594bb07b3faf8d766bb1e9b6bead7cb1081d8 (patch)
tree578cd62b6200a386de57c9bdcf41676c0a9009fd /parsing
parent3fd0490c113432ae3fea6e6defa7b79acb36eae6 (diff)
parentb789106117653fec8340ecbd88866c254fe1201d (diff)
Merge PR #1094: Fixing a little parsing bug with level 90 introduced in 3e70ea9c.
Diffstat (limited to 'parsing')
-rw-r--r--parsing/egramcoq.ml2
-rw-r--r--parsing/g_constr.ml41
2 files changed, 3 insertions, 0 deletions
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 870137ca1..d51b8b54e 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -34,6 +34,7 @@ let default_levels =
[200,Extend.RightA,false;
100,Extend.RightA,false;
99,Extend.RightA,true;
+ 90,Extend.RightA,true;
10,Extend.RightA,false;
9,Extend.RightA,false;
8,Extend.RightA,true;
@@ -44,6 +45,7 @@ let default_pattern_levels =
[200,Extend.RightA,true;
100,Extend.RightA,false;
99,Extend.RightA,true;
+ 90,Extend.RightA,true;
11,Extend.LeftA,false;
10,Extend.RightA,false;
1,Extend.LeftA,false;
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 4e8b98fcf..844c040fd 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -376,6 +376,7 @@ GEXTEND Gram
| "100" RIGHTA
[ 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) ]