X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2Fdiscrimination_tree.mli;h=61631f47869059e0fc0830498d399d83b3b9afab;hb=20ea4afc703668c1c643aaf81d62aeae51be36a1;hp=5c5e6f05d2ca533503fb2ff7c408cbe38660b3db;hpb=b52f57d8573a909a486d52a7317e017f56d07199;p=helm.git

diff --git a/helm/ocaml/cic/discrimination_tree.mli b/helm/ocaml/cic/discrimination_tree.mli
index 5c5e6f05d..61631f478 100644
--- 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