sig
  module TermHashIndex :
    sig
      type index
      type entry = Term.term
      val make_index : unit -> index
      val clear : index -> unit
      val insert : index -> Term.term -> entry -> unit
      val remove_variant : index -> Term.term -> unit
      val iter_all : (entry -> unit) -> index -> unit
      val iter_all_and_throw_away : (entry -> unit) -> index -> unit
      val iter_instance_candidates :
        (entry -> unit) -> index -> Term.term -> Term.context -> unit
      val iter_generalization_candidates :
        (entry -> unit) -> index -> Term.term -> Term.context -> unit
      val iter_unification_candidates :
        (entry -> unit) -> index -> Term.term -> Term.context -> unit
      val size : index -> int
    end
  module TermAlistIndex :
    sig
      type index
      type entry = Term.term
      val make_index : unit -> index
      val clear : index -> unit
      val insert : index -> Term.term -> entry -> unit
      val remove_variant : index -> Term.term -> unit
      val iter_all : (entry -> unit) -> index -> unit
      val iter_all_and_throw_away : (entry -> unit) -> index -> unit
      val iter_instance_candidates :
        (entry -> unit) -> index -> Term.term -> Term.context -> unit
      val iter_generalization_candidates :
        (entry -> unit) -> index -> Term.term -> Term.context -> unit
      val iter_unification_candidates :
        (entry -> unit) -> index -> Term.term -> Term.context -> unit
      val size : index -> int
    end
  type hkey
  module type TableType =
    sig
      type key = DtIndex.hkey
      type 'a t
      val make_table : unit -> 'DtIndex.TableType.t
      val add : 'DtIndex.TableType.t -> DtIndex.TableType.key -> '-> unit
      val remove : 'DtIndex.TableType.t -> DtIndex.TableType.key -> unit
      val find : 'DtIndex.TableType.t -> DtIndex.TableType.key -> 'a
      val iter :
        (DtIndex.TableType.key -> '-> unit) ->
        'DtIndex.TableType.t -> unit
      val iter_and_throw_away :
        (DtIndex.TableType.key -> '-> unit) ->
        'DtIndex.TableType.t -> unit
    end
  module Make :
    functor (Entry : Index.EntryType->
      functor (Table : TableType->
        sig
          type index
          type entry = Entry.entry
          val make_index : unit -> index
          val clear : index -> unit
          val insert : index -> Term.term -> entry -> unit
          val remove_variant : index -> Term.term -> unit
          val iter_all : (entry -> unit) -> index -> unit
          val iter_all_and_throw_away : (entry -> unit) -> index -> unit
          val iter_instance_candidates :
            (entry -> unit) -> index -> Term.term -> Term.context -> unit
          val iter_generalization_candidates :
            (entry -> unit) -> index -> Term.term -> Term.context -> unit
          val iter_unification_candidates :
            (entry -> unit) -> index -> Term.term -> Term.context -> unit
          val size : index -> int
        end
  module HashTableImplementation : TableType
  module AlistTableImplementation : TableType
end