X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2FcicUniv.ml;h=d48772c27a40a0bea41d14eeb0e55de644fb1976;hb=cee1c02ad6a113b711b9d93176296cf16b9ec351;hp=0d75caf898cec408590e0f82a59aaf22bfa4b085;hpb=d0212d7627d3e135c224ffaa30b03ee1969a4578;p=helm.git

diff --git a/helm/software/components/cic/cicUniv.ml b/helm/software/components/cic/cicUniv.ml
index 0d75caf89..d48772c27 100644
--- a/helm/software/components/cic/cicUniv.ml
+++ b/helm/software/components/cic/cicUniv.ml
@@ -397,20 +397,22 @@ let add_gt fast u v b =
 (** Other real code                                                         **)
 (*****************************************************************************)
 
-exception UniverseInconsistency of string 
+exception UniverseInconsistency of string Lazy.t
 
 let error arc node1 closure_type node2 closure =
-  let s = "\n  ===== Universe Inconsistency detected =====\n\n" ^
-   "   Unable to add\n" ^ 
-   "\t" ^ (string_of_arc arc) ^ "\n" ^
-   "   cause\n" ^ 
-   "\t" ^ (string_of_universe node1) ^ "\n" ^
-   "   is in the " ^ closure_type ^ " closure\n" ^
-   "\t{" ^ (string_of_universe_set closure) ^ "}\n" ^ 
-   "   of\n" ^ 
-   "\t" ^ (string_of_universe node2) ^ "\n\n" ^
-   "  ===== Universe Inconsistency detected =====\n" in
-  prerr_endline s;
+  let s =
+   lazy
+    ("\n  ===== Universe Inconsistency detected =====\n\n" ^
+     "   Unable to add\n" ^ 
+     "\t" ^ (string_of_arc arc) ^ "\n" ^
+     "   cause\n" ^ 
+     "\t" ^ (string_of_universe node1) ^ "\n" ^
+     "   is in the " ^ closure_type ^ " closure\n" ^
+     "\t{" ^ (string_of_universe_set closure) ^ "}\n" ^ 
+     "   of\n" ^ 
+     "\t" ^ (string_of_universe node2) ^ "\n\n" ^
+     "  ===== Universe Inconsistency detected =====\n") in
+  prerr_endline (Lazy.force s);
   raise (UniverseInconsistency s)
 
 
@@ -947,7 +949,8 @@ let recons_graph (graph,uriset) =
 
 let assert_univ u =
     match u with 
-    | (_,None) -> raise (UniverseInconsistency "This universe graph has a hole")
+    | (_,None) ->
+       raise (UniverseInconsistency (lazy "This universe graph has a hole"))
     | _ -> ()
     
 let assert_univs_have_uri (graph,_) univlist =