- tactical: [
- [ IDENT "fail" -> return_tactical loc TacticAst.Fail
- | IDENT "do"; count = int; tac = tactical ->
- return_tactical loc (TacticAst.Do (count, tac))
- | IDENT "id" -> return_tactical loc TacticAst.IdTac
- | IDENT "repeat"; tac = tactical ->
- return_tactical loc (TacticAst.Repeat tac)
- | tactics = LIST0 tactical SEP SYMBOL ";" ->
- return_tactical loc (TacticAst.Seq tactics)
- | tac = tactical;
- PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" ->
- return_tactical loc (TacticAst.Then (tac, tacs))
- | IDENT "tries";
- PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" ->
- return_tactical loc (TacticAst.Tries tacs)
- | IDENT "try"; tac = tactical -> return_tactical loc (TacticAst.Try tac)
- | tac = tactic -> return_tactical loc (TacticAst.Tactic tac)
- | PAREN "("; tac = tactical; PAREN ")" -> return_tactical loc tac
- ]
- ];
+ tactical:
+ [ "sequence" LEFTA
+ [ tactics = LIST1 NEXT SEP SYMBOL ";" ->
+ return_tactical loc (TacticAst.Seq tactics)
+ ]
+ | "then" NONA
+ [ tac = tactical;
+ PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" ->
+ return_tactical loc (TacticAst.Then (tac, tacs))
+ ]
+ | "loops" RIGHTA
+ [ IDENT "do"; count = int; tac = tactical ->
+ return_tactical loc (TacticAst.Do (count, tac))
+ | IDENT "repeat"; tac = tactical ->
+ return_tactical loc (TacticAst.Repeat tac)
+ ]
+ | "simple" NONA
+ [ IDENT "tries";
+ PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" ->
+ return_tactical loc (TacticAst.Tries tacs)
+ | IDENT "try"; tac = NEXT -> return_tactical loc (TacticAst.Try tac)
+ | IDENT "fail" -> return_tactical loc TacticAst.Fail
+ | IDENT "id" -> return_tactical loc TacticAst.IdTac
+ | PAREN "("; tac = tactical; PAREN ")" -> return_tactical loc tac
+ | tac = tactic -> return_tactical loc (TacticAst.Tactic tac)
+ ]
+ ];