sig
  type tactic
  module ApplyResult :
    sig
      type apply_result
      val get_num_subgoals : Z3.Tactic.ApplyResult.apply_result -> int
      val get_subgoals :
        Z3.Tactic.ApplyResult.apply_result -> Z3.Goal.goal list
      val get_subgoal :
        Z3.Tactic.ApplyResult.apply_result -> int -> Z3.Goal.goal
      val to_string : Z3.Tactic.ApplyResult.apply_result -> string
    end
  val get_help : Z3.Tactic.tactic -> string
  val get_param_descrs :
    Z3.Tactic.tactic -> Z3.Params.ParamDescrs.param_descrs
  val apply :
    Z3.Tactic.tactic ->
    Z3.Goal.goal ->
    Z3.Params.params option -> Z3.Tactic.ApplyResult.apply_result
  val get_num_tactics : Z3.context -> int
  val get_tactic_names : Z3.context -> string list
  val get_tactic_description : Z3.context -> string -> string
  val mk_tactic : Z3.context -> string -> Z3.Tactic.tactic
  val and_then :
    Z3.context ->
    Z3.Tactic.tactic ->
    Z3.Tactic.tactic -> Z3.Tactic.tactic list -> Z3.Tactic.tactic
  val or_else :
    Z3.context -> Z3.Tactic.tactic -> Z3.Tactic.tactic -> Z3.Tactic.tactic
  val try_for : Z3.context -> Z3.Tactic.tactic -> int -> Z3.Tactic.tactic
  val when_ :
    Z3.context -> Z3.Probe.probe -> Z3.Tactic.tactic -> Z3.Tactic.tactic
  val cond :
    Z3.context ->
    Z3.Probe.probe ->
    Z3.Tactic.tactic -> Z3.Tactic.tactic -> Z3.Tactic.tactic
  val repeat : Z3.context -> Z3.Tactic.tactic -> int -> Z3.Tactic.tactic
  val skip : Z3.context -> Z3.Tactic.tactic
  val fail : Z3.context -> Z3.Tactic.tactic
  val fail_if : Z3.context -> Z3.Probe.probe -> Z3.Tactic.tactic
  val fail_if_not_decided : Z3.context -> Z3.Tactic.tactic
  val using_params :
    Z3.context -> Z3.Tactic.tactic -> Z3.Params.params -> Z3.Tactic.tactic
  val with_ :
    Z3.context -> Z3.Tactic.tactic -> Z3.Params.params -> Z3.Tactic.tactic
  val par_or : Z3.context -> Z3.Tactic.tactic list -> Z3.Tactic.tactic
  val par_and_then :
    Z3.context -> Z3.Tactic.tactic -> Z3.Tactic.tactic -> Z3.Tactic.tactic
  val interrupt : Z3.context -> unit
end