attached auto

[helm.git] / helm / ocaml / tactics / autoTactic.ml

diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml
index 918e7bd71f15d13dcbaa893054e633fc34327b02..50a96d2addd5bb58d5f1bd7da44e32f4f8b02268 100644 (file)
--- a/helm/ocaml/tactics/autoTactic.ml
+++ b/helm/ocaml/tactics/autoTactic.ml
@@ -154,7 +154,7 @@ let rec auto dbd = function
 ;; 
 
 
-let auto_tac  ~(dbd:Mysql.dbd) =
+let auto_tac  ?num ~(dbd:Mysql.dbd) =
   let auto_tac dbh (proof,goal) =
   prerr_endline "Entro in Auto";
   match (auto dbd [(proof, [(goal,depth)],None)]) with