sig
  module HStdecl :
    sig
      type elt = Theory.tdecl
      type t
      val hash : t -> int
      val equal : t -> t -> bool
      val id : t -> int
      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 cardinal : t -> int
      val iter : (elt -> unit) -> t -> unit
      val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
      val fold_left : ('a -> elt -> 'a) -> 'a -> t -> 'a
      val fold_right : (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 min_elt : t -> elt
      val min_elt_opt : t -> elt option
      val max_elt : t -> elt
      val max_elt_opt : t -> elt option
      val choose : t -> elt
      val choose_opt : t -> elt option
      val split : elt -> t -> t * bool * t
      val elements : t -> elt list
      val compare : t -> t -> int
      val to_seq : t -> elt Seq.t
      val to_seq_from : elt -> t -> elt Seq.t
      val add_seq : elt Seq.t -> t -> t
      val of_seq : elt Seq.t -> t
    end
  type tdecl_set = Task.HStdecl.t
  module Wtds :
    sig
      type key = tdecl_set
      type 'a t
      val create : int -> 'a t
      val clear : 'a t -> unit
      val copy : 'a t -> 'a t
      val find : 'a t -> key -> 'a
      val mem : 'a t -> key -> bool
      val set : 'a t -> key -> 'a -> unit
      val remove : 'a t -> key -> unit
      val length : 'a t -> int
      val memoize : int -> (key -> 'a) -> key -> 'a
      val memoize_rec : int -> ((key -> 'a) -> key -> 'a) -> key -> 'a
      val memoize_option : int -> (key option -> 'a) -> key option -> 'a
    end
  val tds_equal : Task.tdecl_set -> Task.tdecl_set -> bool
  val tds_hash : Task.tdecl_set -> int
  val tds_compare : Task.tdecl_set -> Task.tdecl_set -> int
  val tds_empty : Task.tdecl_set
  val mk_tds : Theory.Stdecl.t -> Task.tdecl_set
  type clone_map = Task.tdecl_set Ident.Mid.t
  type meta_map = Task.tdecl_set Theory.Mmeta.t
  type task = Task.task_hd option
  and task_hd = private {
    task_decl : Theory.tdecl;
    task_prev : Task.task;
    task_known : Decl.known_map;
    task_clone : Task.clone_map;
    task_meta : Task.meta_map;
    task_tag : Weakhtbl.tag;
  }
  val task_equal : Task.task -> Task.task -> bool
  val task_hd_equal : Task.task_hd -> Task.task_hd -> bool
  val task_hash : Task.task -> int
  val task_hd_hash : Task.task_hd -> int
  val task_known : Task.task -> Decl.known_map
  val task_clone : Task.task -> Task.clone_map
  val task_meta : Task.task -> Task.meta_map
  val find_clone_tds : Task.task -> Theory.theory -> Task.tdecl_set
  val find_meta_tds : Task.task -> Theory.meta -> Task.tdecl_set
  val add_decl : Task.task -> Decl.decl -> Task.task
  val add_tdecl : Task.task -> Theory.tdecl -> Task.task
  val use_export : Task.task -> Theory.theory -> Task.task
  val clone_export :
    Task.task -> Theory.theory -> Theory.th_inst -> Task.task
  val add_meta :
    Task.task -> Theory.meta -> Theory.meta_arg list -> Task.task
  val add_ty_decl : Task.task -> Ty.tysymbol -> Task.task
  val add_data_decl : Task.task -> Decl.data_decl list -> Task.task
  val add_param_decl : Task.task -> Term.lsymbol -> Task.task
  val add_logic_decl : Task.task -> Decl.logic_decl list -> Task.task
  val add_ind_decl :
    Task.task -> Decl.ind_sign -> Decl.ind_decl list -> Task.task
  val add_prop_decl :
    Task.task -> Decl.prop_kind -> Decl.prsymbol -> Term.term -> Task.task
  val split_theory :
    Theory.theory -> Decl.Spr.t option -> Task.task -> Task.task list
  val used_theories : Task.task -> Theory.theory Ident.Mid.t
  val used_symbols : Theory.theory Ident.Mid.t -> Theory.theory Ident.Mid.t
  val local_decls : Task.task -> Theory.theory Ident.Mid.t -> Decl.decl list
  val task_fold : ('a -> Theory.tdecl -> 'a) -> 'a -> Task.task -> 'a
  val task_iter : (Theory.tdecl -> unit) -> Task.task -> unit
  val task_tdecls : Task.task -> Theory.tdecl list
  val task_decls : Task.task -> Decl.decl list
  val task_goal : Task.task -> Decl.prsymbol
  val task_goal_fmla : Task.task -> Term.term
  val task_separate_goal : Task.task -> Theory.tdecl * Task.task
  val on_meta :
    Theory.meta ->
    ('a -> Theory.meta_arg list -> 'a) -> 'a -> Task.task -> 'a
  val on_cloned_theory :
    Theory.theory -> ('a -> Theory.symbol_map -> 'a) -> 'a -> Task.task -> 'a
  val on_meta_excl : Theory.meta -> Task.task -> Theory.meta_arg list option
  val on_used_theory : Theory.theory -> Task.task -> bool
  val on_tagged_ty : Theory.meta -> Task.task -> Ty.Sty.t
  val on_tagged_ts : Theory.meta -> Task.task -> Ty.Sts.t
  val on_tagged_ls : Theory.meta -> Task.task -> Term.Sls.t
  val on_tagged_pr : Theory.meta -> Task.task -> Decl.Spr.t
  exception NotTaggingMeta of Theory.meta
  exception NotExclusiveMeta of Theory.meta
  exception GoalNotFound
  exception GoalFound
  exception LemmaFound
end