val whd_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
val normalize_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
val unfold_tac:
- ?what:Cic.term -> pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
+ Cic.term option -> pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
val change_tac:
pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic