diff options
| -rw-r--r-- | parsing/g_tactic.ml4 | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 34cdd44d67..a15a6c12df 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -179,6 +179,12 @@ GEXTEND Gram [ [ "["; 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)) *) + let rec pairify = function + | ([]|[_]|[_;_]) as l -> IntroOrAndPattern [l] + | t::q -> IntroOrAndPattern [[t;pairify q]] + in pairify tc | "_" -> IntroWildcard | "?" -> IntroAnonymous | id = ident -> IntroIdentifier id |