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