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"; t1 = tactic_term; t2 = tactic_term;
+ specs = intros_spec ->
+ GrafiteAst.Compose (loc, t1, t2, specs)
| IDENT "constructor"; n = int ->
GrafiteAst.Constructor (loc, n)
| IDENT "contradiction" ->