X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2Fdiscrimination_tree.mli;h=61631f47869059e0fc0830498d399d83b3b9afab;hb=7be6aeb94aa8da17732511a4844bd108976f947f;hp=5c5e6f05d2ca533503fb2ff7c408cbe38660b3db;hpb=1592969317fd01e945bd3dacf775ed4f3144e020;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