From 159d8bc4b82e365934c25c9653abe29b6b6021e0 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 15 Nov 2007 13:44:43 +0000 Subject: [PATCH] removed prerr_endline --- helm/software/components/cic/discrimination_tree.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 *) ;; -- 2.39.2