sig
  module type LayeredIndex =
    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
  module Make :
    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
end