let default_width = 3
(*
-let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:Mysql.dbd)
+let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:HMysql.dbd)
()
=
let auto_tac dbd (proof,goal) =
(fun term -> debug_print (lazy "term_is_equality E` DUMMY!!!!"); false);;
-let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation ~(dbd:Mysql.dbd) () =
+let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation ~(dbd:HMysql.dbd) () =
let auto_tac dbd (proof, goal) =
let normal_auto () =
let universe = MetadataQuery.signature_of_goal ~dbd (proof, goal) in