X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fextlib%2Fdiscrimination_tree.ml;h=f96a0de5695be7f414408b9a582561cbc05a2c2d;hb=c83721701dbbd44d3d547fdec6c4a5658322f424;hp=e0803c3506914b7efa38d0cdbdf69ce5337a9483;hpb=c3fc204cc02f1031b5d17fb0f2be1fc01e5c452f;p=helm.git

diff --git a/helm/software/components/extlib/discrimination_tree.ml b/helm/software/components/extlib/discrimination_tree.ml
index e0803c350..f96a0de56 100644
--- a/helm/software/components/extlib/discrimination_tree.ml
+++ b/helm/software/components/extlib/discrimination_tree.ml
@@ -62,6 +62,7 @@ module type DiscriminationTree =
       type t
 
       val iter : t -> (constant_name path -> dataset -> unit) -> unit
+      val fold : t -> (constant_name path -> dataset -> 'b -> 'b) -> 'b -> 'b
 
       val empty : t
       val index : t -> input -> data -> t
@@ -99,6 +100,8 @@ and type data = A.elt and type dataset = A.t =
 
       let iter dt f = DiscriminationTree.iter (fun p x -> f p x) dt;;
 
+      let fold dt f = DiscriminationTree.fold (fun p x -> f p x) dt;;
+
       let index tree term info =
         let ps = I.path_string_of term in
         let ps_set =