From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 27 Jul 2006 09:10:08 +0000 (+0000)
Subject: print_endline => prerr_endline
X-Git-Tag: 0.4.95@7852~1143
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bd86334840f9c838f02d8c9996ebd9d9e9c43465;p=helm.git

print_endline => prerr_endline
---

diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index 0ffe64e68..90cc85247 100644
--- 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 ba6b2ebe0..02dbf69e0 100644
--- 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);
 ;;