diff options
| author | Hugo Herbelin | 2017-11-26 19:33:00 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2017-11-27 11:27:35 +0100 |
| commit | 257e14b19e9026a4f3cdfa991e27293faf110324 (patch) | |
| tree | 5bce358c8d3a9f359b3a92173b9b60dc2cc8626c | |
| 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.
| -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 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 } -> |