From: Claudio Sacerdoti Coen Date: Thu, 27 Jul 2006 17:34:52 +0000 (+0000) Subject: More debugging output on stderr. X-Git-Tag: make_still_working~6996 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0d1ecc789c6d57a3eef47a028634d316905ef317;p=helm.git More debugging output on stderr. --- 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)) *)