+ theorem_flavour: [ (* all flavours but Goal *)
+ [ [ IDENT "definition" | IDENT "Definition" ] -> `Definition
+ | [ IDENT "fact" | IDENT "Fact" ] -> `Fact
+ | [ IDENT "lemma" | IDENT "Lemma" ] -> `Lemma
+ | [ IDENT "remark" | IDENT "Remark" ] -> `Remark
+ | [ IDENT "theorem" | IDENT "Theorem" ] -> `Theorem
+ ]
+ ];
+ command: [
+ [ [ 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)
+ | [ IDENT "save" | IDENT "Save" ]; name = IDENT ->
+ return_command loc (TacticAst.Qed (Some name))
+ | flavour = theorem_flavour; name = OPT IDENT; SYMBOL ":"; typ = term;
+ body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
+ return_command loc (TacticAst.Theorem (flavour, name, typ, body))
+ | [ IDENT "goal" | IDENT "Goal" ]; typ = term;
+ body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
+ return_command loc (TacticAst.Theorem (`Goal, None, typ, body))
+ | [ IDENT "undo" | IDENT "Undo" ]; steps = OPT NUM ->
+ return_command loc (TacticAst.Undo (int_opt steps))
+ | [ IDENT "redo" | IDENT "Redo" ]; steps = OPT NUM ->
+ return_command loc (TacticAst.Redo (int_opt steps))
+ | [ IDENT "baseuri" | IDENT "Baseuri" ]; uri = OPT QSTRING ->
+ return_command loc (TacticAst.Baseuri uri)
+ | [ IDENT "check" | IDENT "Check" ]; t = term ->
+ return_command loc (TacticAst.Check t)
+ ]
+ ];