From: Alberto Griggio <griggio@fbk.eu>
Date: Mon, 5 Dec 2005 16:49:13 +0000 (+0000)
Subject: better output from main_demod_equalities
X-Git-Tag: make_still_working~8043
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d0c88a989d2c41d0b816c5490d4d8c89a238cb2a;p=helm.git

better output from main_demod_equalities
---

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)))