Coercion hiding implemented. Notes:

[helm.git] / helm / software / components / extlib / discrimination_tree.ml

diff --git a/helm/software/components/extlib/discrimination_tree.ml b/helm/software/components/extlib/discrimination_tree.ml
index e0803c3506914b7efa38d0cdbdf69ce5337a9483..f96a0de5695be7f414408b9a582561cbc05a2c2d 100644 (file)
--- 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 =