sig
  type tdecl_set = private {
    tds_set : Theory.Stdecl.t;
    tds_tag : Weakhtbl.tag;
  }
  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