matitaprover is almost there

[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 537ad02c13e849e6044a1d7a4512f55da4b33d2f..bba9a26aee53ea06c86ca2bf4284f18683476fad 100644 (file)
--- a/helm/software/components/ng_paramodulation/pp.ml
+++ b/helm/software/components/ng_paramodulation/pp.ml
@@ -93,15 +93,15 @@ let pp_unit_clause ~formatter:f c =
       | Terms.Predicate t ->
          Format.fprintf f "@[<hv>{";
          pp_foterm f t;
-         Format.fprintf f "@;[%s] by %s@]"
-            (String.concat ", " (List.map string_of_int vars))
-            (match proof with
-               | Terms.Exact _ -> "axiom"
-               | Terms.Step (rule, id1, id2, _, p, _) -> 
-                   Printf.sprintf "%s %d with %d at %s" 
-                     (string_of_rule rule)
-                     id1 id2 (String.concat
-                               "," (List.map string_of_int p)))
+          Format.fprintf f "@;[%s] by "
+            (String.concat ", " (List.map string_of_int vars));
+          (match proof with
+           | Terms.Exact t -> pp_foterm f t
+           | Terms.Step (rule, id1, id2, _, p, _) -> 
+               Format.fprintf f "%s %d with %d at %s" 
+                 (string_of_rule rule) id1 id2 (String.concat
+                  "," (List.map string_of_int p)));
+          Format.fprintf f "@]"
       | Terms.Equation (lhs, rhs, ty, comp) ->
          Format.fprintf f "@[<hv>{";
          pp_foterm f ty;
@@ -109,15 +109,15 @@ let pp_unit_clause ~formatter:f c =
          pp_foterm f lhs;
           Format.fprintf f "@;%s@;" (string_of_comparison comp);
          pp_foterm f rhs;
-          Format.fprintf f "@]@;[%s] by %s@]"
-            (String.concat ", " (List.map string_of_int vars))
-            (match proof with
-            | Terms.Exact _ -> "axiom"
-            | Terms.Step (rule, id1, id2, _, p, _) -> 
-                 Printf.sprintf "%s %d with %d at %s" 
-                  (string_of_rule rule)
-                  id1 id2 (String.concat
-                 "," (List.map string_of_int p)))
+          Format.fprintf f "@]@;[%s] by "
+            (String.concat ", " (List.map string_of_int vars));
+          (match proof with
+           | Terms.Exact t -> pp_foterm f t
+           | Terms.Step (rule, id1, id2, _, p, _) -> 
+               Format.fprintf f "%s %d with %d at %s" 
+                 (string_of_rule rule) id1 id2 (String.concat
+                  "," (List.map string_of_int p)));
+          Format.fprintf f "@]"
 ;;
 
 let pp_bag ~formatter:f bag =