module DiscriminationTreeIndexing :
functor (A : Set.S) ->
sig
- type path_string_elem = Cic.term
- type path_string = path_string_elem list
val arities : (Cic.term, int) Hashtbl.t
- val path_string_of_term : Cic.term -> Cic.term list
type key = Cic.term
type t
- type elt = A.elt
val empty : t
- val index : t -> Cic.term -> A.elt -> t
- val remove_index : t -> Cic.term -> A.elt -> t
- val in_index : t -> Cic.term -> (A.elt -> bool) -> bool
+ val index : t -> key -> A.elt -> t
+ val remove_index : t -> key -> A.elt -> t
+ val in_index : t -> key -> (A.elt -> bool) -> bool
val retrieve_generalizations : t -> key -> A.t
val retrieve_unifiables : t -> key -> A.t
end