val id_tac : tactic
val fail_tac: tactic
-val first: tactics: (string * tactic) list -> 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
val try_tactic: tactic: tactic -> tactic
-val solve_tactics: tactics: (string * tactic) list -> tactic
+val solve_tactics: tactics: tactic list -> tactic
val progress_tactic: tactic: tactic -> tactic
(* TODO temporary *)