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