AGAIN A TEST

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

diff --git a/helm/software/components/cic/discrimination_tree.ml b/helm/software/components/cic/discrimination_tree.ml
index 92877a8297f8ae0f775e2507cd6d229686731b0c..f5d61463024e3efe957406e6621cbb869de4816a 100644 (file)
--- a/helm/software/components/cic/discrimination_tree.ml
+++ b/helm/software/components/cic/discrimination_tree.ml
@@ -59,7 +59,7 @@ module DiscriminationTreeIndexing =
             assert false (* should not happen *)
         | Cic.LetIn _ | Cic.Lambda _ | Cic.Prod _ | Cic.Cast _
         | Cic.MutCase _ | Cic.Fix _ | Cic.CoFix _ -> 
-            prerr_endline "FIXME: the trie receives an invalid term";
+            HLog.debug "FIXME: the trie receives an invalid term";
             Dead
             (* assert false universe.ml removes these *)
       ;;
@@ -101,6 +101,10 @@ module DiscriminationTreeIndexing =
       type t = A.t DiscriminationTree.t * (path_string_elem*int) list
       let empty = DiscriminationTree.empty, [] ;;
 
+      let iter (dt, _ ) f =
+        DiscriminationTree.iter (fun _ x -> f x) dt
+      ;;
+
       let index (tree,arity) term info =
         let arity,ps = path_string_of_term arity term in
         let ps_set =