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