val lapply_tac:
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
- ?substs:(Cic.name * Cic.term) list -> Cic.term ->
- ProofEngineTypes.tactic
+ ?how_many:int -> ?to_what:Cic.term list -> Cic.term -> ProofEngineTypes.tactic
val fwd_simpl_tac:
- hyp:Cic.name -> dbd:Mysql.dbd -> ProofEngineTypes.tactic
+ ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
+ dbd:Mysql.dbd -> string -> ProofEngineTypes.tactic