-val auto_tac : ?num:int option -> dbd:Mysql.dbd -> ProofEngineTypes.tactic
-val auto_tac_new : dbd:Mysql.dbd -> ProofEngineTypes.tactic
+val auto_tac:
+ ?depth:int -> ?width:int -> ?paramodulation:string -> ?full:string ->
+ dbd:HMysql.dbd -> unit ->
+ ProofEngineTypes.tactic
+