X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Focaml%2Fcic_proof_checking%2FcicEnvironment.ml;h=4a62aaa24741d672e46695cb237ec718557424a3;hb=564d4fe0793c625b9c6be05fa05d5fbb50c61703;hp=c111acd6cf3b75d37c7301a0a90919b02051a2c9;hpb=d922e6065ae8adadf09afbce0f3b2abe72b5bc1c;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
index c111acd6c..4a62aaa24 100644
--- 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
 ;;