sig
  type 'a trans
  type 'a tlist = 'a list Trans.trans
  val store : (Why3.Task.task -> 'a) -> 'a Trans.trans
  val apply : 'a Trans.trans -> Why3.Task.task -> 'a
  val identity : Why3.Task.task Trans.trans
  val identity_l : Why3.Task.task Trans.tlist
  val singleton : 'a Trans.trans -> 'a Trans.tlist
  val return : 'a -> 'a Trans.trans
  val bind : 'a Trans.trans -> ('a -> 'b Trans.trans) -> 'b Trans.trans
  val bind_comp :
    ('a * Why3.Task.task) Trans.trans ->
    ('a -> 'b Trans.trans) -> 'b Trans.trans
  val trace_goal :
    string -> Why3.Task.task Trans.trans -> Why3.Task.task Trans.trans
  val compose :
    Why3.Task.task Trans.trans -> 'a Trans.trans -> 'a Trans.trans
  val compose_l :
    Why3.Task.task Trans.tlist -> 'a Trans.tlist -> 'a Trans.tlist
  val seq : Why3.Task.task Trans.trans list -> Why3.Task.task Trans.trans
  val seq_l : Why3.Task.task Trans.tlist list -> Why3.Task.task Trans.tlist
  val par : Why3.Task.task Trans.trans list -> Why3.Task.task Trans.tlist
  val fold : (Why3.Task.task_hd -> 'a -> 'a) -> 'a -> 'a Trans.trans
  val fold_l : (Why3.Task.task_hd -> 'a -> 'a list) -> 'a -> 'a Trans.tlist
  val fold_decl : (Why3.Decl.decl -> 'a -> 'a) -> 'a -> 'a Trans.trans
  val fold_map :
    (Why3.Task.task_hd -> 'a * 'b -> 'a * 'b) -> 'a -> 'b -> 'b Trans.trans
  val fold_map_l :
    (Why3.Task.task_hd -> 'a * 'b -> ('a * 'b) list) ->
    'a -> 'b -> 'b Trans.tlist
  val decl :
    (Why3.Decl.decl -> Why3.Decl.decl list) ->
    Why3.Task.task -> Why3.Task.task Trans.trans
  val decl_l :
    (Why3.Decl.decl -> Why3.Decl.decl list list) ->
    Why3.Task.task -> Why3.Task.task Trans.tlist
  type diff_decl =
      Goal_decl of Why3.Decl.decl
    | Normal_decl of Why3.Decl.decl
  val decl_goal_l :
    (Why3.Decl.decl -> Trans.diff_decl list list) ->
    Why3.Task.task -> Why3.Task.task Trans.tlist
  val tdecl :
    (Why3.Decl.decl -> Why3.Theory.tdecl list) ->
    Why3.Task.task -> Why3.Task.task Trans.trans
  val tdecl_l :
    (Why3.Decl.decl -> Why3.Theory.tdecl list list) ->
    Why3.Task.task -> Why3.Task.task Trans.tlist
  val goal :
    (Why3.Decl.prsymbol -> Why3.Term.term -> Why3.Decl.decl list) ->
    Why3.Task.task Trans.trans
  val goal_l :
    (Why3.Decl.prsymbol -> Why3.Term.term -> Why3.Decl.decl list list) ->
    Why3.Task.task Trans.tlist
  val tgoal :
    (Why3.Decl.prsymbol -> Why3.Term.term -> Why3.Theory.tdecl list) ->
    Why3.Task.task Trans.trans
  val tgoal_l :
    (Why3.Decl.prsymbol -> Why3.Term.term -> Why3.Theory.tdecl list list) ->
    Why3.Task.task Trans.tlist
  val rewrite :
    (Why3.Term.term -> Why3.Term.term) ->
    Why3.Task.task -> Why3.Task.task Trans.trans
  val rewriteTF :
    (Why3.Term.term -> Why3.Term.term) ->
    (Why3.Term.term -> Why3.Term.term) ->
    Why3.Task.task -> Why3.Task.task Trans.trans
  val add_decls : Why3.Decl.decl list -> Why3.Task.task Trans.trans
  val add_tdecls : Why3.Theory.tdecl list -> Why3.Task.task Trans.trans
  val on_meta :
    Why3.Theory.meta ->
    (Why3.Theory.meta_arg list list -> 'a Trans.trans) -> 'a Trans.trans
  val on_meta_excl :
    Why3.Theory.meta ->
    (Why3.Theory.meta_arg list option -> 'a Trans.trans) -> 'a Trans.trans
  val on_used_theory :
    Why3.Theory.theory -> (bool -> 'a Trans.trans) -> 'a Trans.trans
  val on_cloned_theory :
    Why3.Theory.theory ->
    (Why3.Theory.symbol_map list -> 'a Trans.trans) -> 'a Trans.trans
  val on_tagged_ty :
    Why3.Theory.meta -> (Why3.Ty.Sty.t -> 'a Trans.trans) -> 'a Trans.trans
  val on_tagged_ts :
    Why3.Theory.meta -> (Why3.Ty.Sts.t -> 'a Trans.trans) -> 'a Trans.trans
  val on_tagged_ls :
    Why3.Theory.meta -> (Why3.Term.Sls.t -> 'a Trans.trans) -> 'a Trans.trans
  val on_tagged_pr :
    Why3.Theory.meta -> (Why3.Decl.Spr.t -> 'a Trans.trans) -> 'a Trans.trans
  exception UnknownFlagTrans of Why3.Theory.meta * string * string list
  exception IllegalFlagTrans of Why3.Theory.meta
  type ('a, 'b) flag_trans = ('a -> 'b Trans.trans) Why3.Wstdlib.Hstr.t
  val on_flag :
    Why3.Theory.meta ->
    ('a, 'b) Trans.flag_trans -> string -> 'a -> 'b Trans.trans
  val on_flag_t :
    Why3.Theory.meta ->
    ('a, 'b) Trans.flag_trans ->
    ('a -> 'b Trans.trans) -> 'a -> 'b Trans.trans
  val print_meta :
    Why3.Debug.flag -> Why3.Theory.meta -> Why3.Task.task Trans.trans
  val create_debugging_trans :
    string -> Why3.Task.task Trans.trans -> Why3.Task.task Trans.trans
  exception TransFailure of string * exn
  exception UnknownTrans of string
  exception KnownTrans of string
  val register_env_transform :
    desc:Why3.Pp.formatted ->
    string -> (Why3.Env.env -> Why3.Task.task Trans.trans) -> unit
  val register_env_transform_l :
    desc:Why3.Pp.formatted ->
    string -> (Why3.Env.env -> Why3.Task.task Trans.tlist) -> unit
  val register_transform :
    desc:Why3.Pp.formatted -> string -> Why3.Task.task Trans.trans -> unit
  val register_transform_l :
    desc:Why3.Pp.formatted -> string -> Why3.Task.task Trans.tlist -> unit
  val lookup_transform : string -> Why3.Env.env -> Why3.Task.task Trans.trans
  val lookup_transform_l :
    string -> Why3.Env.env -> Why3.Task.task Trans.tlist
  val list_transforms : unit -> (string * Why3.Pp.formatted) list
  val list_transforms_l : unit -> (string * Why3.Pp.formatted) list
  val named : string -> 'a Trans.trans -> 'a Trans.trans
  type naming_table = {
    namespace : Why3.Theory.namespace;
    known_map : Why3.Decl.known_map;
    coercion : Why3.Coercion.t;
    printer : Why3.Ident.ident_printer;
    aprinter : Why3.Ident.ident_printer;
    meta_id_args : Why3.Ident.ident Why3.Wstdlib.Mstr.t;
  }
  exception Bad_name_table of string
  type trans_with_args =
      string list ->
      Why3.Env.env ->
      Trans.naming_table -> Why3.Env.fformat -> Why3.Task.task Trans.trans
  type trans_with_args_l =
      string list ->
      Why3.Env.env ->
      Trans.naming_table -> Why3.Env.fformat -> Why3.Task.task Trans.tlist
  val list_transforms_with_args : unit -> (string * Why3.Pp.formatted) list
  val list_transforms_with_args_l : unit -> (string * Why3.Pp.formatted) list
  val register_transform_with_args :
    desc:Why3.Pp.formatted -> string -> Trans.trans_with_args -> unit
  val register_transform_with_args_l :
    desc:Why3.Pp.formatted -> string -> Trans.trans_with_args_l -> unit
  type gentrans =
      Trans_one of Why3.Task.task Trans.trans
    | Trans_list of Why3.Task.task Trans.tlist
    | Trans_with_args of Trans.trans_with_args
    | Trans_with_args_l of Trans.trans_with_args_l
  val lookup_trans : Why3.Env.env -> string -> Trans.gentrans
  val lookup_trans_desc : string -> Why3.Pp.formatted
  val list_trans : unit -> string list
  exception Unnecessary_arguments of string list
  val apply_transform :
    string -> Why3.Env.env -> Why3.Task.task -> Why3.Task.task list
  val apply_transform_args :
    string ->
    Why3.Env.env ->
    string list ->
    Trans.naming_table ->
    Why3.Env.fformat -> Why3.Task.task -> Why3.Task.task list
end