From: Enrico Tassi Date: Thu, 15 Jan 2009 15:31:25 +0000 (+0000) Subject: no more universe inconsistency printed to stderr X-Git-Tag: make_still_working~4257 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3d16e43756f5e7c7e551e93e003a15c90627b77b;p=helm.git no more universe inconsistency printed to stderr --- diff --git a/helm/software/components/cic/cicUniv.ml b/helm/software/components/cic/cicUniv.ml index fc01328ab..58dc5cd6c 100644 --- a/helm/software/components/cic/cicUniv.ml +++ b/helm/software/components/cic/cicUniv.ml @@ -317,7 +317,7 @@ let error arc node1 closure_type node2 closure = " of\n" ^ "\t" ^ (string_of_universe node2) ^ "\n\n" ^ " ===== Universe Inconsistency detected =====\n") in - prerr_endline (Lazy.force s); +(* prerr_endline (Lazy.force s); *) raise (UniverseInconsistency s)