module type EqualityIndex =
sig
- module PosEqSet : Set.S with type elt = Utils.pos * Inference.equality
- val arities : (Cic.term, int) Hashtbl.t
- type key = Cic.term
+ module PosEqSet : Set.S with type elt = Utils.pos * Equality.equality
type t = Discrimination_tree.DiscriminationTreeIndexing(PosEqSet).t
val empty : t
- val retrieve_generalizations : t -> key -> PosEqSet.t
- val retrieve_unifiables : t -> key -> PosEqSet.t
+ val retrieve_generalizations : t -> Cic.term -> PosEqSet.t
+ val retrieve_unifiables : t -> Cic.term -> PosEqSet.t
val init_index : unit -> unit
- val remove_index : t -> Inference.equality -> t
- val index : t -> Inference.equality -> t
- val in_index : t -> Inference.equality -> bool
+ val remove_index : t -> Equality.equality -> t
+ val index : t -> Equality.equality -> t
+ val in_index : t -> Equality.equality -> bool
end
module DT : EqualityIndex