X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2Fdiscrimination_tree.ml;h=546f4a34fce9f01b2fcca86ff0148af5ee6ee045;hb=44b1f0c3a1e4bdc0abc3b02004c7b385ab63f7c5;hp=92877a8297f8ae0f775e2507cd6d229686731b0c;hpb=56da33f7a668f84dd0edb335bce9f6fef9a985aa;p=helm.git 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 *) ;;