some more functors and a nice higher-order all_positions iterator

[helm.git] / helm / software / components / ng_paramodulation / pp.ml

diff --git a/helm/software/components/ng_paramodulation/pp.ml b/helm/software/components/ng_paramodulation/pp.ml
index 9dac9001bd6cdea5686f9d2fc122623b2ed8db75..609ca47a7b1a5cce9eff53df81efc39ec71de449 100644 (file)
--- a/helm/software/components/ng_paramodulation/pp.ml
+++ b/helm/software/components/ng_paramodulation/pp.ml
@@ -59,7 +59,9 @@ let pp_substitution ~formatter:f subst =
 let pp_proof bag ~formatter:f p =
   let rec aux eq = function
     | Terms.Exact t -> 
-        Format.fprintf f "%d: Exact (%s)@;" eq (B.pp t)
+        Format.fprintf f "%d: Exact (" eq;
+        pp_foterm f t;
+        Format.fprintf f ")@;";
     | Terms.Step (rule,eq1,eq2,dir,pos,subst) ->
         Format.fprintf f "%d: %s("
           eq (string_of_rule rule);