diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-26 19:33:00 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-27 11:27:35 +0100 |
| commit | 257e14b19e9026a4f3cdfa991e27293faf110324 (patch) | |
| tree | 5bce358c8d3a9f359b3a92173b9b60dc2cc8626c /parsing | |
| parent | 134b220b77d74b0ada801d215a2e5c66bc6726ea (diff) | |
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.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/egramcoq.ml | 1 | ||||
| -rw-r--r-- | parsing/g_constr.ml4 | 7 |
2 files changed, 3 insertions, 5 deletions
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index acbe2d982..9c2766187 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 bfebca2a5..6af8f0b9e 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 } -> |