moved term indexing (in both discrimination and path tree forms) from paramodulation...

[helm.git] / helm / ocaml / cic / discrimination_tree.mli

diff --git a/helm/ocaml/cic/discrimination_tree.mli b/helm/ocaml/cic/discrimination_tree.mli
index 5c5e6f05d2ca533503fb2ff7c408cbe38660b3db..61631f47869059e0fc0830498d399d83b3b9afab 100644 (file)
--- a/helm/ocaml/cic/discrimination_tree.mli
+++ b/helm/ocaml/cic/discrimination_tree.mli
@@ -26,20 +26,16 @@
 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