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