diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_tactic.ml4 | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 672c4eaba8..ebf28e8ebd 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -220,14 +220,18 @@ GEXTEND Gram ; simple_intropattern: [ [ "["; tc = LIST1 intropatterns SEP "|" ; "]" -> IntroOrAndPattern tc - | "("; tc = LIST0 simple_intropattern SEP "," ; ")" -> IntroOrAndPattern [tc] | "()" -> IntroOrAndPattern [[]] - | "{"; tc = LIST0 simple_intropattern SEP "," ; "}" -> - (* {A,B,C} is translated into (A,(B,C)) *) + | "("; si = simple_intropattern; ")" -> IntroOrAndPattern [[si]] + | "("; si = simple_intropattern; ","; + tc = LIST1 simple_intropattern SEP "," ; ")" -> + IntroOrAndPattern [si::tc] + | "("; si = simple_intropattern; "&"; + tc = LIST1 simple_intropattern SEP "&" ; ")" -> + (* (A & B & C) is translated into (A,(B,C)) *) let rec pairify = function | ([]|[_]|[_;_]) as l -> IntroOrAndPattern [l] | t::q -> IntroOrAndPattern [[t;pairify q]] - in pairify tc + in pairify (si::tc) | "_" -> IntroWildcard | prefix = pattern_ident -> IntroFresh prefix | "?" -> IntroAnonymous |