print_endline => prerr_endline

diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index 0ffe64e68e36d50f6ea289edb212235e7ce5c828..90cc852474da915ce94c7645783a39a7d1d8a5a2 100644 (file)
--- a/components/tactics/paramodulation/saturation.ml
+++ b/components/tactics/paramodulation/saturation.ml
@@ -976,7 +976,7 @@ let pp_goals label goals context =
 ;;
 
 let print_status iterno goals active passive =
-  print_endline 
+  prerr_endline 
     (Printf.sprintf "\n%d #ACTIVES: %d #PASSIVES: %d #GOALSET: %d(%d)"
       iterno (size_of_active active) (size_of_passive passive)
       (size_of_goal_set_a goals) (size_of_goal_set_p goals)) 
@@ -1025,7 +1025,7 @@ let given_clause
       in
       match check_if_goals_set_is_solved env active goals with
       | Some p -> 
-          print_endline 
+          prerr_endline 
             (Printf.sprintf "\nFound a proof in: %f\n" 
               (Unix.gettimeofday() -. initial_time));
           ParamodulationSuccess p
@@ -1295,8 +1295,8 @@ let saturate
       raise (ProofEngineTypes.Fail (lazy ("NO proof found: " ^ s)))
   | ParamodulationSuccess 
     (goalproof,newproof,subsumption_id,subsumption_subst, proof_menv) ->
-      print_endline "Proof:";
-      print_endline 
+      prerr_endline "Proof:";
+      prerr_endline 
         (Equality.pp_proof names goalproof newproof subsumption_subst
           subsumption_id type_of_goal);
 (*       prerr_endline "ENDOFPROOFS"; *)
@@ -1414,7 +1414,7 @@ let saturate
           (CicMetaSubst.ppmetasenv [] metasenv)
           (CicMetaSubst.ppmetasenv [] real_metasenv);
 *)
-      print_endline (Printf.sprintf "\nTIME NEEDED: %8.2f" time);
+      prerr_endline (Printf.sprintf "\nTIME NEEDED: %8.2f" time);
       proof, open_goals
 ;;
 
@@ -1544,8 +1544,8 @@ let main_demod_equalities dbd term metasenv ugraph =
       (String.concat "\n"
          (List.map
             (Equality.string_of_equality ~env) equalities));
-    print_endline "--------------------------------------------------";
-    print_endline "GO!";
+    prerr_endline "--------------------------------------------------";
+    prerr_endline "GO!";
     start_time := Unix.gettimeofday ();
     if !time_limit < 1. then time_limit := 60.;    
     let ra, rp =

diff --git a/components/tactics/paramodulation/test_indexing.ml b/components/tactics/paramodulation/test_indexing.ml
index ba6b2ebe062c173735685f50a30f7dab27a2a87c..02dbf69e0b4ccc88b4ed25e171dfc685538bbe38 100644 (file)
--- a/components/tactics/paramodulation/test_indexing.ml
+++ b/components/tactics/paramodulation/test_indexing.ml
@@ -72,7 +72,7 @@ let differing () =
   in
   let res = Inference.extract_differing_subterms t1 t2 in
   match res with
-  | None -> print_endline "NO DIFFERING SUBTERMS???"
+  | None -> prerr_endline "NO DIFFERING SUBTERMS???"
   | Some (t1, t2) ->
       Printf.printf "OK: %s, %s\n" (CicPp.ppterm t1) (CicPp.ppterm t2);
 ;;