From 9d92e1df3dd394def0d8bcb86b04f524e27f98ff Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 16 Jun 2005 15:11:32 +0000 Subject: [PATCH] uses auto_tac_new instead of auto_tac --- helm/matita/matitaEngine.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index a55930fa5..a74df9313 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -49,8 +49,9 @@ let tactic_of_ast = function Tactics.elim_intros term | TacticAst.ElimType (_, term) -> Tactics.elim_type term | TacticAst.Replace (_, what, with_what) -> Tactics.replace ~what ~with_what - | TacticAst.Auto (_,num) -> - AutoTactic.auto_tac ~num (MatitaDb.instance ()) + | TacticAst.Auto (_,depth) -> +(* AutoTactic.auto_tac ~num (MatitaDb.instance ()) *) + AutoTactic.auto_tac_new ?depth ~dbd:(MatitaDb.instance ()) () | TacticAst.Change (_, what, with_what, _) -> Tactics.change ~what ~with_what (* (* TODO Zack a lot more of tactics to be implemented here ... *) -- 2.39.2