diff options
| author | letouzey | 2008-06-01 22:56:50 +0000 |
|---|---|---|
| committer | letouzey | 2008-06-01 22:56:50 +0000 |
| commit | 47ea85e784d83aabddcc9250bfe565833d1e4462 (patch) | |
| tree | c0019ea524a624db1496a7cc0c04ed09d999a9be /parsing | |
| parent | 1b7c478d62af9cc9d3da9ab8512d161be5028a13 (diff) | |
Intropattern: syntax {x,y,z,t} becomes (x & y & z & t), as decided in
a Coq meeting some time ago. NB: this syntax is an alias for (x,(y,(z,t)))
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11033 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |