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