- destruct: core of subst tactic implemented,

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

diff --git a/components/tactics/tacticals.mli b/components/tactics/tacticals.mli
index cdc3bac77f3557b4bc2b65ccb517892be45290e6..800991bb560fa9abd4da4e79399192333352694b 100644 (file)
--- a/components/tactics/tacticals.mli
+++ b/components/tactics/tacticals.mli
@@ -31,6 +31,7 @@ val fail_tac: tactic
 val first: tactics: tactic list -> tactic
 val thens: start: tactic -> continuations: tactic list -> tactic
 val then_: start: tactic -> continuation: tactic -> tactic
+val if_: start: tactic -> continuation: tactic -> fail: tactic -> tactic
 val seq: tactics: tactic list -> tactic (** "folding" of then_ *)
 val repeat_tactic: tactic: tactic -> tactic
 val do_tactic: n: int -> tactic: tactic -> tactic