Tactics.elim_intros_simpl term
| TacticAst.ElimType (_, term) -> Tactics.elim_type term
| TacticAst.Replace (_, what, with_what) -> Tactics.replace ~what ~with_what
-(* | TacticAst.Auto _ -> Tactics.auto_new ~dbd *)
+ | TacticAst.Auto (_,num) ->
+ AutoTactic.auto_tac ~num ~dbd:(MatitaDb.instance ())
| TacticAst.Change (_, what, with_what, _) -> Tactics.change ~what ~with_what
(*
(* TODO Zack a lot more of tactics to be implemented here ... *)
*)
| TacticAst.Intros (loc, num, names) ->
status, TacticAst.Intros (loc, num, names)
- | TacticAst.Auto loc -> status, TacticAst.Auto loc
+ | TacticAst.Auto (loc,num) -> status, TacticAst.Auto (loc,num)
| TacticAst.Reflexivity loc -> status, TacticAst.Reflexivity loc
| TacticAst.Assumption loc -> status, TacticAst.Assumption loc
| TacticAst.Contradiction loc -> status, TacticAst.Contradiction loc