More debug_print made lazy.

[helm.git] / helm / ocaml / cic_proof_checking / cicEnvironment.ml

diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
index c111acd6cf3b75d37c7301a0a90919b02051a2c9..4a62aaa24741d672e46695cb237ec718557424a3 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
@@ -430,18 +430,18 @@ module Cache :
               frozen_list := List.remove_assoc uri !frozen_list;
               frozen_list := (uri,(o,Some real_ugraph))::!frozen_list;
           | Some g -> 
-              debug_print (
+              debug_print (lazy (
                 "You are probably hacking an object already hacked or an"^
                 " object that has the universe file but is not"^
-                " yet committed.");
+                " yet committed."));
               assert false
      with
         Not_found -> 
-          debug_print (
+          debug_print (lazy (
             "You are hacking an object that is not in the"^
             " frozen_list, this means you are probably generating an"^
             " universe file for an object that already"^
-             " as an universe file");
+             " as an universe file"));
           assert false
    ;;
 
@@ -523,8 +523,8 @@ let get_object_to_add uri =
         (Some (CicUniv.ugraph_of_xml filename_univ),Some filename_univ)
     with Failure s ->
       
-      debug_print (
-        "WE HAVE NO UNIVERSE FILE FOR " ^ (UriManager.string_of_uri uri));
+      debug_print (lazy (
+        "WE HAVE NO UNIVERSE FILE FOR " ^ (UriManager.string_of_uri uri)));
         Inix.unlink
       None,None
       *)
@@ -552,21 +552,21 @@ let find_or_add_to_unchecked uri =
 let set_type_checking_info ?(replace_ugraph=None) uri =
 (*
   if not (Cache.can_be_cooked uri) && replace_ugraph <> None then begin
-    debug_print (
+    debug_print (lazy (
       "?replace_ugraph must be None if you are not committing an "^
       "object that has a universe graph associated "^
-      "(can happen only in the fase of universes graphs generation).");
+      "(can happen only in the fase of universes graphs generation)."));
     assert false
   else
 *)
   match Cache.can_be_cooked uri, replace_ugraph with
   | true, Some _
   | false, None ->
-      debug_print (
+      debug_print (lazy (
         "?replace_ugraph must be (Some ugraph) when committing an object that "^
         "has no associated universe graph. If this is in make_univ phase you "^
         "should drop this exception and let univ_make commit thi object with "^
-        "proper arguments");
+        "proper arguments"));
       assert false
   | _ ->
       (match replace_ugraph with 
@@ -602,7 +602,7 @@ let get_cooked_obj ?(trust=true) base_univ uri =
     else
       (* we don't trust the uri, so we fail *)
       begin
-        debug_print ("CACHE MISS: " ^ (UriManager.string_of_uri uri));
+        debug_print (lazy ("CACHE MISS: " ^ (UriManager.string_of_uri uri)));
         raise Not_found
       end
       
@@ -672,6 +672,6 @@ let list_obj () =
     (list_uri ())
   with
     Not_found -> 
-      debug_print "Who has removed the uri in the meanwhile?";
+      debug_print (lazy "Who has removed the uri in the meanwhile?");
       raise Not_found
 ;;