From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 27 Jul 2006 17:34:52 +0000 (+0000)
Subject: More debugging output on stderr.
X-Git-Tag: 0.4.95@7852~1136
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2b4bf09ff59e1bab8b68374133fdacb8283a4fc0;p=helm.git

More debugging output on stderr.
---

diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index 90cc85247..83588d24d 100644
--- a/components/tactics/paramodulation/saturation.ml
+++ b/components/tactics/paramodulation/saturation.ml
@@ -1006,7 +1006,7 @@ let given_clause
     else
       let _ = 
 (*         print_status iterno goals active passive  *)
-        Printf.printf ".%!";
+        Printf.eprintf ".%!";
       in
       (* PRUNING OF PASSIVE THAT WILL NEVER BE PROCESSED *) 
       let passive =
@@ -1538,9 +1538,9 @@ let main_demod_equalities dbd term metasenv ugraph =
     in
     let active = make_active () in
     let passive = make_passive equalities in
-    Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context);
-    Printf.printf "\nmetasenv:\n%s\n" (Utils.print_metasenv metasenv);
-    Printf.printf "\nequalities:\n%s\n"
+    Printf.eprintf "\ncontext:\n%s\n" (PP.ppcontext context);
+    Printf.eprintf "\nmetasenv:\n%s\n" (Utils.print_metasenv metasenv);
+    Printf.eprintf "\nequalities:\n%s\n"
       (String.concat "\n"
          (List.map
             (Equality.string_of_equality ~env) equalities));
@@ -1569,7 +1569,7 @@ let main_demod_equalities dbd term metasenv ugraph =
       let l = fst ra in
       EqualitySet.elements (List.fold_left addfun EqualitySet.empty l)
     in
-    Printf.printf "\n\nRESULTS:\nActive:\n%s\n\nPassive:\n%s\n"
+    Printf.eprintf "\n\nRESULTS:\nActive:\n%s\n\nPassive:\n%s\n"
        (String.concat "\n" (List.map (Equality.string_of_equality ~env) active)) 
      (*  (String.concat "\n"
          (List.map (fun e -> CicPp.ppterm (term_of_equality e)) active)) *)