*)
val auto_tac:
- ?depth:int -> ?width:int -> ?paramodulation:string -> ?full:string ->
- dbd:HMysql.dbd -> unit ->
- ProofEngineTypes.tactic
+ params:(string * string) list
+ -> dbd:HMysql.dbd
+ -> universe:Universe.universe
+ -> ProofEngineTypes.tactic
+val pp_proofterm: Cic.term -> string