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(Cic_indexable.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 -> (Cic_indexable.CicIndexable.constant_name Discrimination_tree.path -> PosEqSet.t -> unit) -> unit
end
module DT =
module PosEqSet = Set.Make(OrderedPosEquality);;
- include Discrimination_tree.DiscriminationTreeIndexing(PosEqSet)
+ include Discrimination_tree.Make(Cic_indexable.CicIndexable)(PosEqSet)
(* DISCRIMINATION TREES *)
module PosEqSet = Set.Make(OrderedPosEquality);;
- include Discrimination_tree.DiscriminationTreeIndexing(PosEqSet)
+ include Discrimination_tree.Make(Cic_indexable.CicIndexable)(PosEqSet)
(* DISCRIMINATION TREES *)