*)
val simpl_tac: pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
-val reduce_tac: pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
val whd_tac: pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
val normalize_tac: pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
+val head_beta_reduce_tac: ?delta:bool -> ?upto:int -> pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
(* The default of term is the thesis of the goal to be prooved *)
val unfold_tac:
pattern:ProofEngineTypes.lazy_pattern ->
ProofEngineTypes.tactic
-val change_tac:
+val change_tac:
+ ?with_cast:bool ->
pattern:ProofEngineTypes.lazy_pattern ->
Cic.lazy_term ->
ProofEngineTypes.tactic