];
tactical0: [ [ t = tactical; SYMBOL "." -> t ] ];
tactical:
- [ "sequence" LEFTA
+ [ "command" NONA
+ [ cmd = command -> return_tactical loc (TacticAst.Command cmd) ]
+ | "sequence" LEFTA
[ tactics = LIST1 NEXT SEP SYMBOL ";" ->
return_tactical loc (TacticAst.Seq tactics)
]
| [ IDENT "id" | IDENT "Id" ] -> return_tactical loc TacticAst.IdTac
| PAREN "("; tac = tactical; PAREN ")" -> return_tactical loc tac
| tac = tactic -> return_tactical loc (TacticAst.Tactic tac)
- | cmd = command -> return_tactical loc (TacticAst.Command cmd)
]
];
theorem_flavour: [ (* all flavours but Goal *)
]
];
command: [
- [ [ IDENT "proof" | IDENT "Proof" ] -> return_command loc TacticAst.Proof
+ [ [ IDENT "abort" | IDENT "Abort" ] -> return_command loc TacticAst.Abort
+ | [ IDENT "proof" | IDENT "Proof" ] -> return_command loc TacticAst.Proof
| [ IDENT "quit" | IDENT "Quit" ] -> return_command loc TacticAst.Quit
| [ IDENT "qed" | IDENT "Qed" ] ->
return_command loc (TacticAst.Qed None)