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)
TacticAst.Exact (loc, t)
| IDENT "exists" ->
TacticAst.Exists loc
- | IDENT "fold"; kind = reduction_kind; t = tactic_term ->
- TacticAst.Fold (loc, kind, t)
+ | IDENT "fail" -> TacticAst.Fail loc
+ | IDENT "fold"; kind = reduction_kind; t = tactic_term;
+ p = OPT [ pattern_spec ] ->
+ let p = match p with None -> [], None | Some p -> p in
+ TacticAst.Fold (loc, kind, t, p)
| IDENT "fourier" ->
TacticAst.Fourier loc
| IDENT "fwd"; t = term ->
TacticAst.Generalize (loc,t,id,p)
| IDENT "goal"; n = NUM ->
TacticAst.Goal (loc, int_of_string n)
+ | IDENT "id" -> TacticAst.IdTac loc
| IDENT "injection"; t = term ->
TacticAst.Injection (loc, t)
| IDENT "intros"; num = OPT [num = int -> num]; idents = OPT ident_list0 ->
TacticAst.Reduce (loc, kind, p)
| IDENT "reflexivity" ->
TacticAst.Reflexivity loc
- | IDENT "replace"; t1 = tactic_term; "with"; t2 = tactic_term ->
- TacticAst.Replace (loc, t1, t2)
+ | IDENT "replace"; p = OPT [ pattern_spec ]; "with"; t = tactic_term ->
+ let p = match p with None -> [], None | Some p -> p in
+ TacticAst.Replace (loc, p, t)
| IDENT "rewrite" ; d = direction; t = term ; p = OPT [ pattern_spec ] ->
let p = match p with None -> [], None | Some p -> p in
TacticAst.Rewrite (loc, d, t, p)
TacticAst.Tries (loc, tacs)
| IDENT "try"; tac = NEXT ->
TacticAst.Try (loc, tac)
- | IDENT "fail" -> TacticAst.Fail loc
- | IDENT "id" -> TacticAst.IdTac loc
| PAREN "("; tac = tactical; PAREN ")" -> tac
| tac = tactic -> TacticAst.Tactic (loc, tac)
]