diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-07-06 13:29:54 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-07-06 13:29:54 +0000 |
| commit | d3eb7c916077eba740d9f35b6ac10358eb0fe934 (patch) | |
| tree | 877cf4de4d51857af42766d8e95ad19e5bb7080b /parsing/g_tactic.ml4 | |
| parent | d5c316353ed1bb63821c511eade468a133a2b480 (diff) | |
Suggestion of additional syntax for intro patterns:
intros {A,B,C,D}
means:
intros (A,(B,(C,D)))
Should be especially useful when breaking existential hypthesis like
{n:nat | P n /\ Q n /\ R n }, hence the notation {}.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9948 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_tactic.ml4')
| -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 34cdd44d6..a15a6c12d 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 |