X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_proof_checking%2FcicEnvironment.ml;h=695e0cffdf293d823013e5148348a289fcd38175;hb=c720c4687a4290cfb85f6c4d2a9f238450ef0d5a;hp=ad61bcd0481795e7b4917b7f330411cc667a259b;hpb=6b3ec8b32b76c40910d7827aae19817d0d579e01;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
index ad61bcd04..695e0cffd 100644
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
@@ -44,7 +44,7 @@ let cleanup_tmp = true;;
 let trust = ref  (fun _ -> true);;
 let set_trust f = trust := f
 let trust_obj uri = !trust uri
-
+let debug_print = fun _ -> ()
 
 (* ************************************************************************** *
                                    TYPES 
@@ -430,14 +430,14 @@ module Cache :
 	       frozen_list := List.remove_assoc uri !frozen_list;
 	       frozen_list := (uri,(o,Some real_ugraph))::!frozen_list;
 	   | Some g -> 
-	       prerr_endline (
+	       debug_print (
 		 "You are probably hacking an object already hacked or an"^
 		 " object that has the universe file but is not"^
 		 " yet committed.");
 	       assert false
      with
 	 Not_found -> 
-	   prerr_endline (
+	   debug_print (
 	     "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"^
@@ -538,7 +538,7 @@ let get_object_to_add uri =
        (Some (CicUniv.ugraph_of_xml filename_univ),Some filename_univ)
    with Failure s ->
      
-     prerr_endline (
+     debug_print (
        "WE HAVE NO UNIVERSE FILE FOR " ^ (UriManager.string_of_uri uri));
        Inix.unlink
      None,None
@@ -567,7 +567,7 @@ 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
-    prerr_endline (
+    debug_print (
       "?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).");
@@ -577,7 +577,7 @@ let set_type_checking_info ?(replace_ugraph=None) uri =
   match Cache.can_be_cooked uri, replace_ugraph with
   | true, Some _
   | false, None ->
-      prerr_endline (
+      debug_print (
         "?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 "^
@@ -617,7 +617,7 @@ let get_cooked_obj ?(trust=true) base_univ uri =
     else
       (* we don't trust the uri, so we fail *)
       begin
-        prerr_endline ("CACHE MISS: " ^ (UriManager.string_of_uri uri));
+        debug_print ("CACHE MISS: " ^ (UriManager.string_of_uri uri));
         raise Not_found
       end
       
@@ -705,6 +705,6 @@ let list_obj () =
     (list_uri ())
   with
     Not_found -> 
-      prerr_endline "Who has removed the uri in the meanwhile?";
+      debug_print "Who has removed the uri in the meanwhile?";
       raise Not_found
 ;;