sig
  type config
  exception ConfigFailure of string * string
  exception DuplicateShortcut of string
  val read_config : string option -> Whyconf.config
  val init_config :
    ?extra_config:string list -> string option -> Whyconf.config
  val read_config_rc : string option -> string * Rc.t
  val add_extra_config : Whyconf.config -> string -> Whyconf.config
  val empty_rc : Rc.t
  val save_config : Whyconf.config -> unit
  val default_config : string -> Whyconf.config
  val get_conf_file : Whyconf.config -> string
  val rc_of_config : Whyconf.config -> Rc.t
  type main
  val get_main : Whyconf.config -> Whyconf.main
  val set_main : Whyconf.config -> Whyconf.main -> Whyconf.config
  val set_stdlib : bool -> Whyconf.config -> Whyconf.config
  val set_load_default_plugins : bool -> Whyconf.config -> Whyconf.config
  val libdir : Whyconf.main -> string
  val set_libdir : Whyconf.main -> string -> Whyconf.main
  val datadir : Whyconf.main -> string
  val set_datadir : Whyconf.main -> string -> Whyconf.main
  val loadpath : Whyconf.main -> string list
  val set_loadpath : Whyconf.main -> string list -> Whyconf.main
  val timelimit : Whyconf.main -> float
  val memlimit : Whyconf.main -> int
  val running_provers_max : Whyconf.main -> int
  val set_limits : Whyconf.main -> float -> int -> int -> Whyconf.main
  val stdlib_path : string Stdlib.ref
  val default_editor : Whyconf.main -> string
  val set_default_editor : Whyconf.main -> string -> Whyconf.main
  val plugins : Whyconf.main -> string list
  val pluginsdir : Whyconf.main -> string
  val set_plugins : Whyconf.main -> string list -> Whyconf.main
  val add_plugin : Whyconf.main -> string -> Whyconf.main
  val load_plugins : Whyconf.main -> unit
  type prover = {
    prover_name : string;
    prover_version : string;
    prover_altern : string;
  }
  val print_prover : Stdlib.Format.formatter -> Whyconf.prover -> unit
  val print_prover_parseable_format :
    Stdlib.Format.formatter -> Whyconf.prover -> unit
  val prover_parseable_format : Whyconf.prover -> string
  module Prover :
    sig
      type t = prover
      val hash : t -> int
      val equal : t -> t -> bool
      val compare : t -> t -> int
    end
  module Mprover :
    sig
      type key = prover
      type +'a t
      val empty : 'a t
      val is_empty : 'a t -> bool
      val mem : key -> 'a t -> bool
      val add : key -> 'a -> 'a t -> 'a t
      val singleton : key -> 'a -> 'a t
      val remove : key -> 'a t -> 'a t
      val merge :
        (key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
      val union : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
      val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
      val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
      val iter : (key -> 'a -> unit) -> 'a t -> unit
      val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
      val for_all : (key -> 'a -> bool) -> 'a t -> bool
      val exists : (key -> 'a -> bool) -> 'a t -> bool
      val filter : (key -> 'a -> bool) -> 'a t -> 'a t
      val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
      val cardinal : 'a t -> int
      val bindings : 'a t -> (key * 'a) list
      val min_binding : 'a t -> key * 'a
      val max_binding : 'a t -> key * 'a
      val choose : 'a t -> key * 'a
      val split : key -> 'a t -> 'a t * 'a option * 'a t
      val find : key -> 'a t -> 'a
      val map : ('a -> 'b) -> 'a t -> 'b t
      val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
      val change : ('a option -> 'a option) -> key -> 'a t -> 'a t
      val inter : (key -> 'a -> 'b -> 'c option) -> 'a t -> 'b t -> 'c t
      val diff : (key -> 'a -> 'b -> 'a option) -> 'a t -> 'b t -> 'a t
      val submap : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
      val disjoint : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
      val set_union : 'a t -> 'a t -> 'a t
      val set_inter : 'a t -> 'b t -> 'a t
      val set_diff : 'a t -> 'b t -> 'a t
      val set_submap : 'a t -> 'b t -> bool
      val set_disjoint : 'a t -> 'b t -> bool
      val set_compare : 'a t -> 'b t -> int
      val set_equal : 'a t -> 'b t -> bool
      val find_def : 'a -> key -> 'a t -> 'a
      val find_opt : key -> 'a t -> 'a option
      val find_exn : exn -> key -> 'a t -> 'a
      val map_filter : ('a -> 'b option) -> 'a t -> 'b t
      val mapi_filter : (key -> 'a -> 'b option) -> 'a t -> 'b t
      val mapi_fold :
        (key -> 'a -> 'acc -> 'acc * 'b) -> 'a t -> 'acc -> 'acc * 'b t
      val mapi_filter_fold :
        (key -> 'a -> 'acc -> 'acc * 'b option) ->
        'a t -> 'acc -> 'acc * 'b t
      val fold_left : ('b -> key -> 'a -> 'b) -> 'b -> 'a t -> 'b
      val fold_right : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
      val fold2_inter :
        (key -> 'a -> 'b -> 'c -> 'c) -> 'a t -> 'b t -> 'c -> 'c
      val fold2_union :
        (key -> 'a option -> 'b option -> 'c -> 'c) ->
        'a t -> 'b t -> 'c -> 'c
      val translate : (key -> key) -> 'a t -> 'a t
      val add_new : exn -> key -> 'a -> 'a t -> 'a t
      val replace : exn -> key -> 'a -> 'a t -> 'a t
      val keys : 'a t -> key list
      val values : 'a t -> 'a list
      val of_list : (key * 'a) list -> 'a t
      val contains : 'a t -> key -> bool
      val domain : 'a t -> unit t
      val subdomain : (key -> 'a -> bool) -> 'a t -> unit t
      val is_num_elt : int -> 'a t -> bool
      type 'a enumeration
      val val_enum : 'a enumeration -> (key * 'a) option
      val start_enum : 'a t -> 'a enumeration
      val next_enum : 'a enumeration -> 'a enumeration
      val start_ge_enum : key -> 'a t -> 'a enumeration
      val next_ge_enum : key -> 'a enumeration -> 'a enumeration
    end
  module Sprover :
    sig
      module M :
        sig
          type key = prover
          type 'a t = 'a Mprover.t
          val empty : 'a t
          val is_empty : 'a t -> bool
          val mem : key -> 'a t -> bool
          val add : key -> 'a -> 'a t -> 'a t
          val singleton : key -> 'a -> 'a t
          val remove : key -> 'a t -> 'a t
          val merge :
            (key -> 'a option -> 'b option -> 'c option) ->
            'a t -> 'b t -> 'c t
          val union : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
          val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
          val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
          val iter : (key -> 'a -> unit) -> 'a t -> unit
          val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
          val for_all : (key -> 'a -> bool) -> 'a t -> bool
          val exists : (key -> 'a -> bool) -> 'a t -> bool
          val filter : (key -> 'a -> bool) -> 'a t -> 'a t
          val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
          val cardinal : 'a t -> int
          val bindings : 'a t -> (key * 'a) list
          val min_binding : 'a t -> key * 'a
          val max_binding : 'a t -> key * 'a
          val choose : 'a t -> key * 'a
          val split : key -> 'a t -> 'a t * 'a option * 'a t
          val find : key -> 'a t -> 'a
          val map : ('a -> 'b) -> 'a t -> 'b t
          val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
          val change : ('a option -> 'a option) -> key -> 'a t -> 'a t
          val inter : (key -> 'a -> 'b -> 'c option) -> 'a t -> 'b t -> 'c t
          val diff : (key -> 'a -> 'b -> 'a option) -> 'a t -> 'b t -> 'a t
          val submap : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
          val disjoint : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
          val set_union : 'a t -> 'a t -> 'a t
          val set_inter : 'a t -> 'b t -> 'a t
          val set_diff : 'a t -> 'b t -> 'a t
          val set_submap : 'a t -> 'b t -> bool
          val set_disjoint : 'a t -> 'b t -> bool
          val set_compare : 'a t -> 'b t -> int
          val set_equal : 'a t -> 'b t -> bool
          val find_def : 'a -> key -> 'a t -> 'a
          val find_opt : key -> 'a t -> 'a option
          val find_exn : exn -> key -> 'a t -> 'a
          val map_filter : ('a -> 'b option) -> 'a t -> 'b t
          val mapi_filter : (key -> 'a -> 'b option) -> 'a t -> 'b t
          val mapi_fold :
            (key -> 'a -> 'acc -> 'acc * 'b) -> 'a t -> 'acc -> 'acc * 'b t
          val mapi_filter_fold :
            (key -> 'a -> 'acc -> 'acc * 'b option) ->
            'a t -> 'acc -> 'acc * 'b t
          val fold_left : ('b -> key -> 'a -> 'b) -> 'b -> 'a t -> 'b
          val fold_right : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
          val fold2_inter :
            (key -> 'a -> 'b -> 'c -> 'c) -> 'a t -> 'b t -> 'c -> 'c
          val fold2_union :
            (key -> 'a option -> 'b option -> 'c -> 'c) ->
            'a t -> 'b t -> 'c -> 'c
          val translate : (key -> key) -> 'a t -> 'a t
          val add_new : exn -> key -> 'a -> 'a t -> 'a t
          val replace : exn -> key -> 'a -> 'a t -> 'a t
          val keys : 'a t -> key list
          val values : 'a t -> 'a list
          val of_list : (key * 'a) list -> 'a t
          val contains : 'a t -> key -> bool
          val domain : 'a t -> unit t
          val subdomain : (key -> 'a -> bool) -> 'a t -> unit t
          val is_num_elt : int -> 'a t -> bool
          type 'a enumeration = 'a Mprover.enumeration
          val val_enum : 'a enumeration -> (key * 'a) option
          val start_enum : 'a t -> 'a enumeration
          val next_enum : 'a enumeration -> 'a enumeration
          val start_ge_enum : key -> 'a t -> 'a enumeration
          val next_ge_enum : key -> 'a enumeration -> 'a enumeration
        end
      type elt = M.key
      type t = unit M.t
      val empty : t
      val is_empty : t -> bool
      val mem : elt -> t -> bool
      val add : elt -> t -> t
      val singleton : elt -> t
      val remove : elt -> t -> t
      val merge : (elt -> bool -> bool -> bool) -> t -> t -> t
      val compare : t -> t -> int
      val equal : t -> t -> bool
      val subset : t -> t -> bool
      val disjoint : t -> t -> bool
      val iter : (elt -> unit) -> t -> unit
      val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
      val for_all : (elt -> bool) -> t -> bool
      val exists : (elt -> bool) -> t -> bool
      val filter : (elt -> bool) -> t -> t
      val partition : (elt -> bool) -> t -> t * t
      val cardinal : t -> int
      val elements : t -> elt list
      val min_elt : t -> elt
      val max_elt : t -> elt
      val choose : t -> elt
      val split : elt -> t -> t * bool * t
      val change : (bool -> bool) -> elt -> t -> t
      val union : t -> t -> t
      val inter : t -> t -> t
      val diff : t -> t -> t
      val fold_left : ('b -> elt -> 'b) -> 'b -> t -> 'b
      val fold_right : (elt -> 'a -> 'a) -> t -> 'a -> 'a
      val fold2_inter : (elt -> 'a -> 'a) -> t -> t -> 'a -> 'a
      val fold2_union : (elt -> 'a -> 'a) -> t -> t -> 'a -> 'a
      val translate : (elt -> elt) -> t -> t
      val add_new : exn -> elt -> t -> t
      val is_num_elt : int -> t -> bool
      val of_list : elt list -> t
      val contains : t -> elt -> bool
      val add_left : t -> elt -> t
      val remove_left : t -> elt -> t
      val print :
        (Format.formatter -> elt -> unit) -> Format.formatter -> t -> unit
    end
  module Hprover :
    sig
      type key = prover
      type !'a t
      val create : int -> 'a t
      val clear : 'a t -> unit
      val reset : 'a t -> unit
      val copy : 'a t -> 'a t
      val add : 'a t -> key -> 'a -> unit
      val remove : 'a t -> key -> unit
      val find : 'a t -> key -> 'a
      val find_all : 'a t -> key -> 'a list
      val replace : 'a t -> key -> 'a -> unit
      val mem : 'a t -> key -> bool
      val iter : (key -> 'a -> unit) -> 'a t -> unit
      val filter_map_inplace : (key -> 'a -> 'a option) -> 'a t -> unit
      val fold : (key -> 'a -> 'acc -> 'acc) -> 'a t -> 'acc -> 'acc
      val length : 'a t -> int
      val stats : 'a t -> Hashtbl.statistics
      val to_seq : 'a t -> (key * 'a) Seq.t
      val to_seq_keys : 'a t -> key Seq.t
      val to_seq_values : 'a t -> 'a Seq.t
      val add_seq : 'a t -> (key * 'a) Seq.t -> unit
      val replace_seq : 'a t -> (key * 'a) Seq.t -> unit
      val of_seq : (key * 'a) Seq.t -> 'a t
      val find_def : 'a t -> 'a -> key -> 'a
      val find_opt : 'a t -> key -> 'a option
      val find_exn : 'a t -> exn -> key -> 'a
      val map : (key -> 'a -> 'b) -> 'a t -> 'b t
      val memo : int -> (key -> 'a) -> key -> 'a
      val is_empty : 'a t -> bool
    end
  type config_prover = {
    prover : Whyconf.prover;
    command : string;
    command_steps : string option;
    driver : string option * string;
    in_place : bool;
    editor : string;
    interactive : bool;
    extra_options : string list;
    extra_drivers : (string * string list) list;
  }
  val get_complete_command :
    Whyconf.config_prover -> with_steps:bool -> string
  val get_provers : Whyconf.config -> Whyconf.config_prover Whyconf.Mprover.t
  val get_prover_config :
    Whyconf.config -> Whyconf.prover -> Whyconf.config_prover
  val set_provers :
    Whyconf.config ->
    ?shortcuts:Whyconf.prover Wstdlib.Mstr.t ->
    Whyconf.config_prover Whyconf.Mprover.t -> Whyconf.config
  val add_provers :
    Whyconf.config ->
    Whyconf.config_prover Whyconf.Mprover.t ->
    Whyconf.prover Wstdlib.Mstr.t -> Whyconf.config
  val is_prover_known : Whyconf.config -> Whyconf.prover -> bool
  val get_prover_shortcuts : Whyconf.config -> Whyconf.prover Wstdlib.Mstr.t
  val set_prover_shortcuts :
    Whyconf.config -> Whyconf.prover Wstdlib.Mstr.t -> Whyconf.config
  type config_editor = {
    editor_name : string;
    editor_command : string;
    editor_options : string list;
  }
  module Meditor :
    sig
      type key = string
      type +'a t
      val empty : 'a t
      val is_empty : 'a t -> bool
      val mem : key -> 'a t -> bool
      val add : key -> 'a -> 'a t -> 'a t
      val singleton : key -> 'a -> 'a t
      val remove : key -> 'a t -> 'a t
      val merge :
        (key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
      val union : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
      val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
      val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
      val iter : (key -> 'a -> unit) -> 'a t -> unit
      val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
      val for_all : (key -> 'a -> bool) -> 'a t -> bool
      val exists : (key -> 'a -> bool) -> 'a t -> bool
      val filter : (key -> 'a -> bool) -> 'a t -> 'a t
      val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
      val cardinal : 'a t -> int
      val bindings : 'a t -> (key * 'a) list
      val min_binding : 'a t -> key * 'a
      val max_binding : 'a t -> key * 'a
      val choose : 'a t -> key * 'a
      val split : key -> 'a t -> 'a t * 'a option * 'a t
      val find : key -> 'a t -> 'a
      val map : ('a -> 'b) -> 'a t -> 'b t
      val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
      val change : ('a option -> 'a option) -> key -> 'a t -> 'a t
      val inter : (key -> 'a -> 'b -> 'c option) -> 'a t -> 'b t -> 'c t
      val diff : (key -> 'a -> 'b -> 'a option) -> 'a t -> 'b t -> 'a t
      val submap : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
      val disjoint : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
      val set_union : 'a t -> 'a t -> 'a t
      val set_inter : 'a t -> 'b t -> 'a t
      val set_diff : 'a t -> 'b t -> 'a t
      val set_submap : 'a t -> 'b t -> bool
      val set_disjoint : 'a t -> 'b t -> bool
      val set_compare : 'a t -> 'b t -> int
      val set_equal : 'a t -> 'b t -> bool
      val find_def : 'a -> key -> 'a t -> 'a
      val find_opt : key -> 'a t -> 'a option
      val find_exn : exn -> key -> 'a t -> 'a
      val map_filter : ('a -> 'b option) -> 'a t -> 'b t
      val mapi_filter : (key -> 'a -> 'b option) -> 'a t -> 'b t
      val mapi_fold :
        (key -> 'a -> 'acc -> 'acc * 'b) -> 'a t -> 'acc -> 'acc * 'b t
      val mapi_filter_fold :
        (key -> 'a -> 'acc -> 'acc * 'b option) ->
        'a t -> 'acc -> 'acc * 'b t
      val fold_left : ('b -> key -> 'a -> 'b) -> 'b -> 'a t -> 'b
      val fold_right : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
      val fold2_inter :
        (key -> 'a -> 'b -> 'c -> 'c) -> 'a t -> 'b t -> 'c -> 'c
      val fold2_union :
        (key -> 'a option -> 'b option -> 'c -> 'c) ->
        'a t -> 'b t -> 'c -> 'c
      val translate : (key -> key) -> 'a t -> 'a t
      val add_new : exn -> key -> 'a -> 'a t -> 'a t
      val replace : exn -> key -> 'a -> 'a t -> 'a t
      val keys : 'a t -> key list
      val values : 'a t -> 'a list
      val of_list : (key * 'a) list -> 'a t
      val contains : 'a t -> key -> bool
      val domain : 'a t -> unit t
      val subdomain : (key -> 'a -> bool) -> 'a t -> unit t
      val is_num_elt : int -> 'a t -> bool
      type 'a enumeration
      val val_enum : 'a enumeration -> (key * 'a) option
      val start_enum : 'a t -> 'a enumeration
      val next_enum : 'a enumeration -> 'a enumeration
      val start_ge_enum : key -> 'a t -> 'a enumeration
      val next_ge_enum : key -> 'a enumeration -> 'a enumeration
    end
  val set_editors :
    Whyconf.config ->
    Whyconf.config_editor Whyconf.Meditor.t -> Whyconf.config
  val get_editors : Whyconf.config -> Whyconf.config_editor Whyconf.Meditor.t
  val editor_by_id : Whyconf.config -> string -> Whyconf.config_editor
  val set_prover_editors :
    Whyconf.config -> string Whyconf.Mprover.t -> Whyconf.config
  val get_prover_editors : Whyconf.config -> string Whyconf.Mprover.t
  val get_prover_editor : Whyconf.config -> Whyconf.prover -> string
  type prover_upgrade_policy =
      CPU_keep
    | CPU_upgrade of Whyconf.prover
    | CPU_duplicate of Whyconf.prover
    | CPU_remove
  val print_prover_upgrade_policy :
    Stdlib.Format.formatter -> Whyconf.prover_upgrade_policy -> unit
  val set_prover_upgrade_policy :
    Whyconf.config ->
    Whyconf.prover -> Whyconf.prover_upgrade_policy -> Whyconf.config
  val get_prover_upgrade_policy :
    Whyconf.config -> Whyconf.prover -> Whyconf.prover_upgrade_policy
  val get_policies :
    Whyconf.config -> Whyconf.prover_upgrade_policy Whyconf.Mprover.t
  val set_policies :
    Whyconf.config ->
    Whyconf.prover_upgrade_policy Whyconf.Mprover.t -> Whyconf.config
  type config_strategy = {
    strategy_name : string;
    strategy_desc : string;
    strategy_code : string;
    strategy_shortcut : string;
  }
  val get_strategies :
    Whyconf.config -> Whyconf.config_strategy Wstdlib.Mstr.t
  val add_strategy :
    Whyconf.config -> Whyconf.config_strategy -> Whyconf.config
  type filter_prover
  val mk_filter_prover :
    ?version:string -> ?altern:string -> string -> Whyconf.filter_prover
  val print_filter_prover :
    Stdlib.Format.formatter -> Whyconf.filter_prover -> unit
  val parse_filter_prover : string -> Whyconf.filter_prover
  val filter_prover_with_shortcut :
    Whyconf.config -> Whyconf.filter_prover -> Whyconf.filter_prover
  val filter_prover : Whyconf.filter_prover -> Whyconf.prover -> bool
  val filter_provers :
    Whyconf.config ->
    Whyconf.filter_prover -> Whyconf.config_prover Whyconf.Mprover.t
  exception ProverNotFound of Whyconf.config * Whyconf.filter_prover
  exception ProverAmbiguity of Whyconf.config * Whyconf.filter_prover *
              Whyconf.config_prover Whyconf.Mprover.t
  exception ParseFilterProver of string
  val filter_one_prover :
    Whyconf.config -> Whyconf.filter_prover -> Whyconf.config_prover
  val why3_regexp_of_string : string -> Re.Str.regexp
  module User :
    sig
      val update_section :
        Rc.t -> string -> (Rc.section -> Rc.section) -> Rc.t
      val set_prover_editor :
        Whyconf.config -> Whyconf.Mprover.key -> string -> Whyconf.config
      val set_default_editor : Whyconf.config -> string -> Whyconf.config
      val set_limits :
        time:float -> mem:int -> j:int -> Whyconf.config -> Whyconf.config
      val set_prover_upgrade_policy :
        Whyconf.config ->
        Whyconf.Mprover.key ->
        Whyconf.prover_upgrade_policy -> Whyconf.config
      val remove_user_policy :
        Whyconf.config -> Whyconf.Mprover.key -> Whyconf.config
      val get_section : Whyconf.config -> string -> Rc.section option
      val get_simple_family : Whyconf.config -> string -> Rc.section list
      val get_family : Whyconf.config -> string -> Rc.family
      val set_section :
        Whyconf.config -> string -> Rc.section -> Whyconf.config
      val set_simple_family :
        Whyconf.config -> string -> Rc.section list -> Whyconf.config
      val set_family :
        Whyconf.config -> string -> Rc.family -> Whyconf.config
    end
  module type Command = functor () -> sig end
  val commands : (module Whyconf.Command) Wstdlib.Hstr.t
  val register_command : string -> (module Whyconf.Command) -> unit
  module Args :
    sig
      val first_arg : int Stdlib.ref
      val opt_config : string option Stdlib.ref
      val add_command : string -> unit
      val all_options :
        Getopt.opt list -> string -> string -> Getopt.opt list
      val initialize :
        ?extra_help:string ->
        Getopt.opt list ->
        (string -> unit) -> string -> Whyconf.config * Env.env
      val complete_initialization : unit -> Whyconf.config * Env.env
      val exit_with_usage : ?extra_help:string -> string -> 'a
      val common_options : Getopt.opt list
    end
  val unknown_to_known_provers :
    Whyconf.config_prover Whyconf.Mprover.t ->
    Whyconf.prover ->
    Whyconf.prover list * Whyconf.prover list * Whyconf.prover list
  val provers_from_detected_provers :
    (Whyconf.config -> Rc.t -> Whyconf.config) Stdlib.ref
end