-val whd :
- also_in_hypotheses:bool ->
- terms:Cic.term list option -> ProofEngineTypes.tactic
-val normalize :
- also_in_hypotheses:bool ->
- terms:Cic.term list option -> ProofEngineTypes.tactic
-val fwd_simpl : hyp:Cic.name -> dbd:Mysql.dbd -> ProofEngineTypes.tactic
-val lapply :
- ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
- ?substs:(Cic.name * Cic.term) list -> Cic.term -> ProofEngineTypes.tactic