GrafiteAst.ApplyS (loc, t, params)
| IDENT "assumption" ->
GrafiteAst.Assumption loc
- | IDENT "auto"; params = auto_params ->
- GrafiteAst.Auto (loc,params)
+ | IDENT "autobatch"; params = auto_params ->
+ 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" ->
let prefix = match prefix with None -> "" | Some prefix -> prefix in
GrafiteAst.Inline (loc,style,suri,prefix)
| [ IDENT "hint" ] -> GrafiteAst.Hint loc
+ | IDENT "auto"; params = auto_params ->
+ GrafiteAst.AutoInteractive (loc,params)
| [ IDENT "whelp"; "match" ] ; t = term ->
GrafiteAst.WMatch (loc,t)
| [ IDENT "whelp"; IDENT "instance" ] ; t = term ->