sig
  type entry
  type index
  val make_index : unit -> LayeredIndex.LayeredIndex.index
  val clear : LayeredIndex.LayeredIndex.index -> unit
  val insert :
    LayeredIndex.LayeredIndex.index ->
    Term.term -> LayeredIndex.LayeredIndex.entry -> unit
  val remove_variant : LayeredIndex.LayeredIndex.index -> Term.term -> unit
  val iter_all :
    (LayeredIndex.LayeredIndex.entry -> unit) ->
    LayeredIndex.LayeredIndex.index -> unit
  val iter_all_and_throw_away :
    (LayeredIndex.LayeredIndex.entry -> unit) ->
    LayeredIndex.LayeredIndex.index -> unit
  val iter_instance_candidates :
    (LayeredIndex.LayeredIndex.entry -> unit) ->
    LayeredIndex.LayeredIndex.index -> Term.term -> Term.context -> unit
  val iter_generalization_candidates :
    (LayeredIndex.LayeredIndex.entry -> unit) ->
    LayeredIndex.LayeredIndex.index -> Term.term -> Term.context -> unit
  val iter_unification_candidates :
    (LayeredIndex.LayeredIndex.entry -> unit) ->
    LayeredIndex.LayeredIndex.index -> Term.term -> Term.context -> unit
  val size : LayeredIndex.LayeredIndex.index -> int
  type state
  val obtain_state :
    LayeredIndex.LayeredIndex.index -> LayeredIndex.LayeredIndex.state
  val install_state : LayeredIndex.LayeredIndex.state -> unit
  val add_layer :
    LayeredIndex.LayeredIndex.state -> LayeredIndex.LayeredIndex.state
  val new_layer :
    LayeredIndex.LayeredIndex.index -> LayeredIndex.LayeredIndex.state
end