- [ [ IDENT "absurd" | IDENT "Absurd" ]; t = tactic_term ->
- return_tactic loc (TacticAst.Absurd t)
- | [ IDENT "apply" | IDENT "Apply" ]; t = tactic_term ->
- return_tactic loc (TacticAst.Apply t)
- | [ IDENT "assumption" | IDENT "Assumption" ] ->
- return_tactic loc TacticAst.Assumption
- | [ IDENT "auto" | IDENT "Auto" ] -> return_tactic loc TacticAst.Auto
- | [ IDENT "change" | IDENT "Change" ];
- t1 = tactic_term; "with"; t2 = tactic_term;
- where = tactic_where ->
- return_tactic loc (TacticAst.Change (t1, t2, where))
- (* TODO Change_pattern *)
- | [ IDENT "contradiction" | IDENT "Contradiction" ] ->
- return_tactic loc TacticAst.Contradiction
- | [ IDENT "cut" | IDENT "Cut" ];
- t = tactic_term -> return_tactic loc (TacticAst.Cut t)
- | [ IDENT "decompose" | IDENT "Decompose" ];
- principles = ident_list1; where = IDENT ->
- return_tactic loc (TacticAst.Decompose (where, principles))
- | [ IDENT "discriminate" | IDENT "Discriminate" ];
- hyp = IDENT ->
- return_tactic loc (TacticAst.Discriminate hyp)
- | [ IDENT "elimType" | IDENT "ElimType" ]; t = tactic_term ->
- return_tactic loc (TacticAst.ElimType t)
- | [ IDENT "elim" | IDENT "Elim" ];
- t1 = tactic_term;
+ [ IDENT "absurd"; t = tactic_term ->
+ TacticAst.Absurd (loc, t)
+ | IDENT "apply"; t = tactic_term ->
+ TacticAst.Apply (loc, t)
+ | IDENT "assumption" ->
+ TacticAst.Assumption loc
+ | IDENT "auto";
+ depth = OPT [ IDENT "depth"; SYMBOL "="; i = NUM -> int_of_string i ];
+ width = OPT [ IDENT "depth"; SYMBOL "="; i = NUM -> int_of_string i ] ->
+ TacticAst.Auto (loc,depth,width)
+ | IDENT "clear"; id = IDENT ->
+ TacticAst.Clear (loc,id)
+ | IDENT "clearbody"; id = IDENT ->
+ TacticAst.ClearBody (loc,id)
+ | IDENT "change"; t1 = tactic_term; "with"; t2 = tactic_term; "in";
+ where = pattern_spec ->
+ TacticAst.Change (loc, t1, t2, where)
+ | IDENT "compare"; t = tactic_term ->
+ TacticAst.Compare (loc,t)
+ | IDENT "constructor"; n = NUM ->
+ TacticAst.Constructor (loc,int_of_string n)
+ | IDENT "contradiction" ->
+ TacticAst.Contradiction loc
+ | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
+ TacticAst.Cut (loc, ident, t)
+ | IDENT "decide"; IDENT "equality" ->
+ TacticAst.DecideEquality loc
+ | IDENT "decompose"; where = term ->
+ TacticAst.Decompose (loc, where)
+ | IDENT "discriminate"; t = tactic_term ->
+ TacticAst.Discriminate (loc, t)
+ | IDENT "elim"; t1 = tactic_term;