module type EqualityIndex =
sig
module PosEqSet : Set.S with type elt = Utils.pos * Equality.equality
- type t = Discrimination_tree.DiscriminationTreeIndexing(Discrimination_tree.CicIndexable)(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