elim tactic: it needs two arguments, a term as well as a pattern

[helm.git] / components / tactics / reductionTactics.mli

diff --git a/components/tactics/reductionTactics.mli b/components/tactics/reductionTactics.mli
index 16e2bc23c475694e8b70a0a2d73dd02e0c0a61d3..62200df69a0cfc3d6e843fae3ad0acc114d7fe4e 100644 (file)
--- a/components/tactics/reductionTactics.mli
+++ b/components/tactics/reductionTactics.mli
@@ -27,6 +27,7 @@ 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: