From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 16 Jun 2005 15:11:32 +0000 (+0000)
Subject: uses auto_tac_new instead of auto_tac
X-Git-Tag: INDEXING_NO_PROOFS~131
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9d92e1df3dd394def0d8bcb86b04f524e27f98ff;p=helm.git

uses auto_tac_new instead of auto_tac
---

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 ... *)