sig
  type instruction =
      Icall_prover of
        (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 *
        (Env.env -> Task.task -> Strategy.proof_tree)
    | Scall_prover of
        (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 = Env.env -> Task.task -> Strategy.proof_tree
  type strat_with_args =
      string list ->
      Env.env ->
      Trans.naming_table -> Env.fformat -> Task.task -> Strategy.proof_tree
  val register_strat : desc:Pp.formatted -> string -> Strategy.strat -> unit
  val register_strat_with_args :
    desc: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 * Pp.formatted) list
end