better output from main_demod_equalities

diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml
index 10d76faa1295522168ceae334cb12b5cd0689f48..9e533d8d635bd1c707706eec04107b37afb70e1b 100644 (file)
--- 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)))