X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Ftacticals.mli;h=44a6ab4d9cffb0160bd1deaa1ae64359725e4363;hb=f9abd21eb0d26cf9b632af4df819225be4d091e3;hp=cdc3bac77f3557b4bc2b65ccb517892be45290e6;hpb=50afaf262195266d156f594cff7e92a6e8898b3e;p=helm.git

diff --git a/helm/software/components/tactics/tacticals.mli b/helm/software/components/tactics/tacticals.mli
index cdc3bac77..44a6ab4d9 100644
--- a/helm/software/components/tactics/tacticals.mli
+++ b/helm/software/components/tactics/tacticals.mli
@@ -31,6 +31,8 @@ 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 ifs: start: tactic -> continuations: tactic list -> fail: 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