diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:38:16 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:38:16 +0000 |
| commit | fafd9c0fbc366185fe3bf9697524687a65e0b7c2 (patch) | |
| tree | 0955a17dcd6f2a3efee11604431f0ccbcf5a2368 /parsing/g_ltac.ml4 | |
| parent | 8bec4e3fac58fd96c876a22634e5b25a566e9ce1 (diff) | |
Added the tactical "tac1 + tac2".
It works pretty much like "tac1 || tac2" except that it has as successes all the successes of tac1 followed by all the successes of tac2 (whereas the latter has either the successes of tac1 (if there is at least one) or those of tac2 (otherwise)).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16998 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_ltac.ml4')
| -rw-r--r-- | parsing/g_ltac.ml4 | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index e0a1c046a..96f4bc387 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -73,7 +73,9 @@ GEXTEND Gram TacAbstract (tc,Some s) ] (*End of To do*) | "2" RIGHTA - [ ta0 = tactic_expr; "||"; ta1 = binder_tactic -> TacOrelse (ta0,ta1) + [ ta0 = tactic_expr; "+"; ta1 = binder_tactic -> TacOr (ta0,ta1) + | ta0 = tactic_expr; "+"; ta1 = tactic_expr -> TacOr (ta0,ta1) + | ta0 = tactic_expr; "||"; ta1 = binder_tactic -> TacOrelse (ta0,ta1) | ta0 = tactic_expr; "||"; ta1 = tactic_expr -> TacOrelse (ta0,ta1) ] | "1" RIGHTA [ b = match_key; IDENT "goal"; "with"; mrl = match_context_list; "end" -> |