sig
  type instruction =
      Icall_prover of
        (Why3.Whyconf.prover * float option * int option * int option) list
    | Itransform of string * int
    | Igoto of int
  type t = Strategy.instruction array
  type proof_tree =
      Sdo_nothing
    | Sapply_trans of string * string list * Strategy.proof_tree list
    | Scont of string * string list *
        (Why3.Env.env -> Why3.Task.task -> Strategy.proof_tree)
    | Scall_prover of
        (Why3.Whyconf.prover * float option * int option * int option) list *
        Strategy.proof_tree
  exception StratFailure of string * exn
  exception UnknownStrat of string
  exception KnownStrat of string
  type strat = Why3.Env.env -> Why3.Task.task -> Strategy.proof_tree
  type strat_with_args =
      string list ->
      Why3.Env.env ->
      Why3.Trans.naming_table ->
      Why3.Env.fformat -> Why3.Task.task -> Strategy.proof_tree
  val register_strat :
    desc:Why3.Pp.formatted -> string -> Strategy.strat -> unit
  val register_strat_with_args :
    desc:Why3.Pp.formatted -> string -> Strategy.strat_with_args -> unit
  type gen_strat =
      Strat of Strategy.strat
    | StratWithArgs of Strategy.strat_with_args
  val lookup_strat : string -> Strategy.gen_strat
  val list_strats : unit -> (string * Why3.Pp.formatted) list
end