val lapply_tac:
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
- Cic.term -> ProofEngineTypes.tactic
+ ?how_many:int -> ?to_what:Cic.term list -> Cic.term -> ProofEngineTypes.tactic
val fwd_simpl_tac:
- term:Cic.term -> dbd:Mysql.dbd -> ProofEngineTypes.tactic
+ ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
+ dbd:Mysql.dbd -> string -> ProofEngineTypes.tactic