From 0d1ecc789c6d57a3eef47a028634d316905ef317 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 27 Jul 2006 17:34:52 +0000 Subject: [PATCH] More debugging output on stderr. --- .../components/tactics/paramodulation/saturation.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) 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)) *) -- 2.39.2