GrafiteAst.AutoBatch (loc,params)
| IDENT "cases"; what = tactic_term;
specs = intros_spec ->
- GrafiteAst.Cases (loc, what, specs)
+ GrafiteAst.Cases (loc, what, specs)
| IDENT "clear"; ids = LIST1 IDENT ->
GrafiteAst.Clear (loc, ids)
| IDENT "clearbody"; id = IDENT ->
GrafiteAst.ClearBody (loc,id)
| IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
GrafiteAst.Change (loc, what, t)
+ | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 =
+ OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec ->
+ let times = match times with None -> 1 | Some i -> i in
+ GrafiteAst.Compose (loc, t1, t2, times, specs)
| IDENT "constructor"; n = int ->
GrafiteAst.Constructor (loc, n)
| IDENT "contradiction" ->