Tactics.applyS ~term ~params ~dbd:(LibraryDb.instance ())
~universe:status.GrafiteTypes.universe
| GrafiteAst.Assumption _ -> Tactics.assumption
- | GrafiteAst.Auto (_,params) ->
- AutoTactic.auto_tac ~params ~dbd:(LibraryDb.instance ())
+ | GrafiteAst.AutoBatch (_,params) ->
+ Tactics.auto ~params ~dbd:(LibraryDb.instance ())
~universe:status.GrafiteTypes.universe
| GrafiteAst.Cases (_, what, (howmany, names)) ->
Tactics.cases_intros ?howmany ~mk_fresh_name_callback:(namer_of names)
status,[]
| GrafiteAst.Print (_,"proofterm") ->
let _,_,_,p,_, _ = GrafiteTypes.get_current_proof status in
- print_endline (AutoTactic.pp_proofterm p);
+ print_endline (Auto.pp_proofterm p);
status,[]
| GrafiteAst.Print (_,_) -> status,[]
| GrafiteAst.Qed loc ->