end
;;
+let default_depth = 5
+let default_width = 3
-let auto_tac_new ~(dbd:Mysql.dbd) =
+let auto_tac_new ?(depth=default_depth) ?(width=default_width) ~(dbd:Mysql.dbd)
+ ()
+=
let auto_tac dbd (proof,goal) =
Hashtbl.clear inspected_goals;
debug_print "Entro in Auto";