];
tactical:
[ "sequence" LEFTA
- [ tactical = NEXT -> tactical
- | tacticals = LIST1 NEXT SEP SYMBOL ";" -> TacticAst.Seq (loc, tacticals)
+ [ tacticals = LIST1 NEXT SEP SYMBOL ";" ->
+ match tacticals with
+ [] -> assert false
+ | [tac] -> tac
+ | l -> TacticAst.Seq (loc, l)
]
| "then" NONA
- [ tac = tactical;
+ [ tac = tactical; SYMBOL ";";
PAREN "["; tacs = LIST0 tactical SEP SYMBOL "|"; PAREN "]" ->
(TacticAst.Then (loc, tac, tacs))
]
TacticAst.Repeat (loc, tac)
]
| "simple" NONA
- [ IDENT "tries";
- PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" ->
- TacticAst.Tries (loc, tacs)
+ [ IDENT "first";
+ PAREN "["; tacs = LIST0 tactical SEP SYMBOL "|"; PAREN "]" ->
+ TacticAst.First (loc, tacs)
| IDENT "try"; tac = NEXT ->
TacticAst.Try (loc, tac)
+ | IDENT "solve";
+ PAREN "["; tacs = LIST0 tactical SEP SYMBOL "|"; PAREN "]" ->
+ TacticAst.Solve (loc, tacs)
| PAREN "("; tac = tactical; PAREN ")" -> tac
| tac = tactic -> TacticAst.Tactic (loc, tac)
]