From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 15 Nov 2007 13:44:43 +0000 (+0000)
Subject: removed prerr_endline
X-Git-Tag: make_still_working~5837
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=159d8bc4b82e365934c25c9653abe29b6b6021e0;p=helm.git

removed prerr_endline
---

diff --git a/helm/software/components/cic/discrimination_tree.ml b/helm/software/components/cic/discrimination_tree.ml
index 92877a829..546f4a34f 100644
--- 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 *)
       ;;