...

[helm.git] / helm / software / components / ng_refiner / nDiscriminationTree.mli

diff --git a/helm/software/components/ng_refiner/nDiscriminationTree.mli b/helm/software/components/ng_refiner/nDiscriminationTree.mli
index a146c4b730771145da58d21c65b72fec5a7da488..04f8c690786de74921ec6171d5d0ec9eb2b0a239 100644 (file)
--- a/helm/software/components/ng_refiner/nDiscriminationTree.mli
+++ b/helm/software/components/ng_refiner/nDiscriminationTree.mli
@@ -12,12 +12,16 @@
 
 (* $Id$ *)
 
+type path_string
+
+val pp_path_string : path_string -> string
+
 module DiscriminationTreeIndexing :
   functor (A : Set.S) ->
     sig
 
       type t 
-      val iter : t -> (A.t -> unit) -> unit
+      val iter : t -> (path_string -> A.t -> unit) -> unit
 
       val empty : t
       val index : t -> NCic.term -> A.elt -> t