X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fsaturation.ml;h=83588d24d5a7987da65242326adeda5a9bf07567;hb=0d1ecc789c6d57a3eef47a028634d316905ef317;hp=90cc852474da915ce94c7645783a39a7d1d8a5a2;hpb=d348c454be6bae89169ed2948067e62e33f62bd8;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index 90cc85247..83588d24d 100644
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/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)) *)