val lapply_tac:
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
- Cic.term -> ProofEngineTypes.tactic
+ ?to_what:Cic.term -> Cic.term -> ProofEngineTypes.tactic
val fwd_simpl_tac:
what:Cic.term -> dbd:Mysql.dbd -> ProofEngineTypes.tactic