functor (LayerType : Index.Index->
  sig
    type entry = LayerType.entry
    type index
    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
    type state
    val obtain_state : index -> state
    val install_state : state -> unit
    val add_layer : state -> state
    val new_layer : index -> state
  end