From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 19 Mar 2008 17:44:49 +0000 (+0000)
Subject: prerr_endline => debug_print
X-Git-Tag: make_still_working~5524
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=00f768086a4aa9373a16a30f5b3898095b5ca14d;p=helm.git

prerr_endline => debug_print
---

diff --git a/helm/software/components/tactics/metadataQuery.ml b/helm/software/components/tactics/metadataQuery.ml
index abe192b94..2941a806e 100644
--- a/helm/software/components/tactics/metadataQuery.ml
+++ b/helm/software/components/tactics/metadataQuery.ml
@@ -288,20 +288,20 @@ let universe_of_goal ~(dbd:HSql.dbd) apply_only metasenv goal =
   let uris =
     Constr.UriManagerSet.fold
       (fun u acc -> 
-         prerr_endline ("processing "^(UriManager.string_of_uri u));
+         debug_print (lazy ("processing "^(UriManager.string_of_uri u)));
          let set_for_sigmatch = 
 	   Constr.UriManagerSet.remove u all_constants_closed in
 	 if LibraryObjects.is_eq_URI (UriManager.strip_xpointer u) then
 	   (* equality has a special treatment *)
-           (prerr_endline "special treatment";
+           (debug_print (lazy "special treatment");
 	   let tfe =
 	     Constr.SetSet.elements (types_for_equality metasenv goal) 
 	   in
 	     List.fold_left 
 	       (fun acc l ->
 		  let tyl = Constr.UriManagerSet.elements l in
-                  prerr_endline ("tyl: "^(String.concat "\n" 
-			(List.map UriManager.string_of_uri tyl)));
+                  debug_print (lazy ("tyl: "^(String.concat "\n" 
+			(List.map UriManager.string_of_uri tyl))));
 		  let set_for_sigmatch =
 		    Constr.UriManagerSet.diff set_for_sigmatch l in
 		  let uris =
@@ -310,7 +310,7 @@ let universe_of_goal ~(dbd:HSql.dbd) apply_only metasenv goal =
 		    acc @ uris) 
 	       acc tfe)
 	 else
-           (prerr_endline "normal treatment";
+           (debug_print (lazy "normal treatment");
            let uris =
              sigmatch ~dbd ~facts:false ~where:`Statement 
                (Some (u,[]),set_for_sigmatch)