- | [ IDENT "auto" ] ; num = OPT [ i = NUM -> int_of_string i ] ->
- TacticAst.Auto (loc,num)
- | [ IDENT "change" ];
- t1 = tactic_term; "with"; t2 = tactic_term; where = pattern_spec ->
- TacticAst.Change (loc, t1, t2, where)
- (* TODO Change_pattern *)
- | [ IDENT "contradiction" ] ->
+ | IDENT "auto";
+ depth = OPT [ IDENT "depth"; SYMBOL "="; i = NUM -> int_of_string i ];
+ width = OPT [ IDENT "width"; 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"; what = pattern_spec; "with"; t = tactic_term ->
+ TacticAst.Change (loc, what, t)
+ | IDENT "compare"; t = tactic_term ->
+ TacticAst.Compare (loc,t)
+ | IDENT "constructor"; n = NUM ->
+ TacticAst.Constructor (loc,int_of_string n)
+ | IDENT "contradiction" ->