From 4965352c558f8e030b3b968f98566f87ed6f0b8a Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 20 Apr 2020 18:29:57 +0200 Subject: do not print debug stuff --- backend/Profilingaux.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'backend/Profilingaux.ml') diff --git a/backend/Profilingaux.ml b/backend/Profilingaux.ml index f8fc5d6b..ec0ae304 100644 --- a/backend/Profilingaux.ml +++ b/backend/Profilingaux.ml @@ -24,8 +24,10 @@ let print_anonymous_function pp f = let function_id (f : coq_function) : identifier = let digest = Digest.string (Marshal.to_string f []) in + (* Printf.fprintf stderr "FUNCTION hash = %a\n" pp_id digest; print_anonymous_function stderr f; + *) digest let branch_id (f_id : identifier) (node : P.t) : identifier = @@ -65,7 +67,7 @@ let load_profiling_info (filename : string) : unit = let condition_oracle (id : identifier) : bool option = let (count0, count1) = get_counts id in - ( (* if count0 <> 0L || count1 <> 0L then *) - Printf.fprintf stderr "%a : %Ld %Ld\n" pp_id id count0 count1); + (* (if count0 <> 0L || count1 <> 0L then + Printf.fprintf stderr "%a : %Ld %Ld\n" pp_id id count0 count1); *) if count0 = count1 then None else Some(count1 > count0);; -- cgit