sig
  type t
  type elt
  module Leaf :
    sig
      type t
      type elt = elt
      val empty : t
      val add : t -> term -> elt -> t
      val remove : t -> term -> elt -> t
      val is_empty : t -> bool
      val iter : t -> (term -> elt -> unit) -> unit
      val fold : t -> 'a -> ('a -> term -> elt -> 'a) -> 'a
      val size : t -> int
      val fold_unify :
        ?subst:subst ->
        t Scoped.t -> term Scoped.t -> (term * elt * subst) Sequence.t
      val fold_match :
        ?subst:subst ->
        t Scoped.t -> term Scoped.t -> (term * elt * subst) Sequence.t
      val fold_matched :
        ?subst:subst ->
        t Scoped.t -> term Scoped.t -> (term * elt * subst) Sequence.t
    end
  val name : string
  val empty : unit -> Index_intf.TERM_IDX.t
  val is_empty : Index_intf.TERM_IDX.t -> bool
  val size : Index_intf.TERM_IDX.t -> int
  val add :
    Index_intf.TERM_IDX.t ->
    Index_intf.term -> Index_intf.TERM_IDX.elt -> Index_intf.TERM_IDX.t
  val add_seq :
    Index_intf.TERM_IDX.t ->
    (Index_intf.term * Index_intf.TERM_IDX.elt) Sequence.t ->
    Index_intf.TERM_IDX.t
  val add_list :
    Index_intf.TERM_IDX.t ->
    (Index_intf.term * Index_intf.TERM_IDX.elt) list -> Index_intf.TERM_IDX.t
  val remove :
    Index_intf.TERM_IDX.t ->
    Index_intf.term -> Index_intf.TERM_IDX.elt -> Index_intf.TERM_IDX.t
  val iter :
    Index_intf.TERM_IDX.t ->
    (Index_intf.term -> Index_intf.TERM_IDX.elt -> unit) -> unit
  val fold :
    Index_intf.TERM_IDX.t ->
    ('a -> Index_intf.term -> Index_intf.TERM_IDX.elt -> 'a) -> 'a -> 'a
  val retrieve_unifiables :
    ?subst:Index_intf.subst ->
    Index_intf.TERM_IDX.t Scoped.t ->
    Index_intf.term Scoped.t ->
    (Index_intf.term * Index_intf.TERM_IDX.elt * Index_intf.subst) Sequence.t
  val retrieve_generalizations :
    ?subst:Index_intf.subst ->
    Index_intf.TERM_IDX.t Scoped.t ->
    Index_intf.term Scoped.t ->
    (Index_intf.term * Index_intf.TERM_IDX.elt * Index_intf.subst) Sequence.t
  val retrieve_specializations :
    ?subst:Index_intf.subst ->
    Index_intf.TERM_IDX.t Scoped.t ->
    Index_intf.term Scoped.t ->
    (Index_intf.term * Index_intf.TERM_IDX.elt * Index_intf.subst) Sequence.t
  val to_dot :
    Index_intf.TERM_IDX.elt CCFormat.printer ->
    Index_intf.TERM_IDX.t CCFormat.printer
end