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