- transcript: patched to generate CoRN_notation.ma instead of CoRN.ma

[helm.git] / helm / software / components / cic / cicUniv.ml

diff --git a/helm/software/components/cic/cicUniv.ml b/helm/software/components/cic/cicUniv.ml
index 0d75caf898cec408590e0f82a59aaf22bfa4b085..d48772c27a40a0bea41d14eeb0e55de644fb1976 100644 (file)
--- 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 =