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
(* DISCRIMINATION TREES *)
- let init_index () =
- Hashtbl.clear arities;
- ;;
+ let init_index () = () ;;
let remove_index tree equality =
let _, _, (_, l, r, ordering), _,_ = Equality.open_equality equality in
(* DISCRIMINATION TREES *)
- let init_index () =
- Hashtbl.clear arities;
- ;;
+ let init_index () = () ;;
let remove_index tree equality =
let _, _, (_, l, r, ordering), _,_ = Equality.open_equality equality in