]> matita.cs.unibo.it Git - helm.git/commitdiff
uses auto_tac_new instead of auto_tac
authorStefano Zacchiroli <zack@upsilon.cc>
Thu, 16 Jun 2005 15:11:32 +0000 (15:11 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Thu, 16 Jun 2005 15:11:32 +0000 (15:11 +0000)
helm/matita/matitaEngine.ml

index a55930fa52299446a5e9167f1f521b5e6081302a..a74df9313cc5a05755e1a883f836dfe0cb4d92e6 100644 (file)
@@ -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 ... *)