diff options
| author | Clément Pit-Claudel | 2019-10-28 12:53:31 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2019-10-28 12:53:31 -0400 |
| commit | 6c5de19692ba7c7b00c650ed02f3b4136cbf81fc (patch) | |
| tree | de44fba242c42d1c6f35d2b9559e896314d1b64d /parsing | |
| parent | 073b259e8ffb898257f16fc3412caf24f271d7a1 (diff) | |
| parent | 74c6d69a08b50b77c001ca758d25f1a969bf2c73 (diff) | |
Merge PR #10963: Possible simplification of parsing rules.
Reviewed-by: ppedrot
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_constr.mlg | 16 |
1 files changed, 4 insertions, 12 deletions
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index ea44e748c9..87b9a8eea3 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -196,17 +196,11 @@ GRAMMAR EXTEND Gram [ "200" RIGHTA [ c = binder_constr -> { c } ] | "100" RIGHTA - [ c1 = operconstr; "<:"; c2 = binder_constr -> + [ c1 = operconstr; "<:"; c2 = operconstr LEVEL "200" -> { CAst.make ~loc @@ CCast(c1, CastVM c2) } - | c1 = operconstr; "<:"; c2 = SELF -> - { CAst.make ~loc @@ CCast(c1, CastVM c2) } - | c1 = operconstr; "<<:"; c2 = binder_constr -> - { CAst.make ~loc @@ CCast(c1, CastNative c2) } - | c1 = operconstr; "<<:"; c2 = SELF -> + | c1 = operconstr; "<<:"; c2 = operconstr LEVEL "200" -> { CAst.make ~loc @@ CCast(c1, CastNative c2) } - | c1 = operconstr; ":";c2 = binder_constr -> - { CAst.make ~loc @@ CCast(c1, CastConv c2) } - | c1 = operconstr; ":"; c2 = SELF -> + | c1 = operconstr; ":"; c2 = operconstr LEVEL "200" -> { CAst.make ~loc @@ CCast(c1, CastConv c2) } | c1 = operconstr; ":>" -> { CAst.make ~loc @@ CCast(c1, CastCoerce) } ] @@ -407,9 +401,7 @@ GRAMMAR EXTEND Gram pattern: [ "200" RIGHTA [ ] | "100" RIGHTA - [ p = pattern; ":"; ty = binder_constr -> - {CAst.make ~loc @@ CPatCast (p, ty) } - | p = pattern; ":"; ty = operconstr LEVEL "100" -> + [ p = pattern; ":"; ty = operconstr LEVEL "200" -> {CAst.make ~loc @@ CPatCast (p, ty) } ] | "99" RIGHTA [ ] | "90" RIGHTA [ ] |