module type EqualityIndex =
sig
module PosEqSet : Set.S with type elt = Utils.pos * Equality.equality
- type t = Discrimination_tree.DiscriminationTreeIndexing(PosEqSet).t
+ type t = Discrimination_tree.Make(Discrimination_tree.CicIndexable)(PosEqSet).t
val empty : t
val retrieve_generalizations : t -> Cic.term -> PosEqSet.t
val retrieve_unifiables : t -> Cic.term -> PosEqSet.t
val remove_index : t -> Equality.equality -> t
val index : t -> Equality.equality -> t
val in_index : t -> Equality.equality -> bool
- val iter : t -> (Discrimination_tree.path -> PosEqSet.t -> unit) -> unit
+ val iter : t -> (Discrimination_tree.CicIndexable.constant_name Discrimination_tree.path -> PosEqSet.t -> unit) -> unit
end
module DT : EqualityIndex