*)
val auto_tac:
- params:(string * string) list ->
- dbd:HMysql.dbd ->
- ProofEngineTypes.tactic
+ params:(string * string) list
+ -> dbd:HMysql.dbd
+ -> universe:Universe.universe
+ -> ProofEngineTypes.tactic
-val applyS_tac: dbd:HMysql.dbd -> term: Cic.term -> ProofEngineTypes.tactic
+val pp_proofterm: Cic.term -> string