module type EqualityIndex =
sig
module PosEqSet : Set.S with type elt = Utils.pos * Equality.equality
- val arities : (Cic.term, int) Hashtbl.t
- type key = Cic.term
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 -> Equality.equality -> t
val index : t -> Equality.equality -> t