From d0c88a989d2c41d0b816c5490d4d8c89a238cb2a Mon Sep 17 00:00:00 2001 From: Alberto Griggio Date: Mon, 5 Dec 2005 16:49:13 +0000 Subject: [PATCH] better output from main_demod_equalities --- helm/ocaml/paramodulation/saturation.ml | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index 10d76faa1..9e533d8d6 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/paramodulation/saturation.ml @@ -2359,15 +2359,18 @@ let main_demod_equalities dbd term metasenv ugraph = match rp with | (n, _), (p, _), _ -> EqualitySet.elements (List.fold_left addfun EqualitySet.empty p) - | _ -> assert false in let active = let l = List.map snd (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" - (String.concat "\n" (List.map (string_of_equality ~env) active)) - (String.concat "\n" (List.map (string_of_equality ~env) passive)); +(* (String.concat "\n" (List.map (string_of_equality ~env) active)) *) + (String.concat "\n" + (List.map (fun e -> CicPp.ppterm (term_of_equality e)) active)) +(* (String.concat "\n" (List.map (string_of_equality ~env) passive)); *) + (String.concat "\n" + (List.map (fun e -> CicPp.ppterm (term_of_equality e)) passive)); print_newline (); with e -> debug_print (lazy ("EXCEPTION: " ^ (Printexc.to_string e))) -- 2.39.2