]> matita.cs.unibo.it Git - helm.git/commitdiff
removed prerr_endline
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 15 Nov 2007 13:44:43 +0000 (13:44 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 15 Nov 2007 13:44:43 +0000 (13:44 +0000)
components/cic/discrimination_tree.ml

index 92877a8297f8ae0f775e2507cd6d229686731b0c..546f4a34fce9f01b2fcca86ff0148af5ee6ee045 100644 (file)
@@ -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 *)
       ;;