From 59d4332991ab14755fa631d729edb5b5d3c6714c Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 27 Jul 2006 09:10:08 +0000 Subject: [PATCH] print_endline => prerr_endline --- .../tactics/paramodulation/saturation.ml | 14 +++++++------- .../tactics/paramodulation/test_indexing.ml | 2 +- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml index 0ffe64e68..90cc85247 100644 --- a/helm/software/components/tactics/paramodulation/saturation.ml +++ b/helm/software/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/helm/software/components/tactics/paramodulation/test_indexing.ml b/helm/software/components/tactics/paramodulation/test_indexing.ml index ba6b2ebe0..02dbf69e0 100644 --- a/helm/software/components/tactics/paramodulation/test_indexing.ml +++ b/helm/software/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); ;; -- 2.39.2