val reduce_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
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
val change_tac:
pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic