removed debug prerr_endline

[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 ad61bcd0481795e7b4917b7f330411cc667a259b..695e0cffdf293d823013e5148348a289fcd38175 100644 (file)
--- 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
 ;;