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