Ported demodulation on clauses

[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 d93fade272e9479be851a5dbb33853f6d26ecf8e..5008489df828b48c95b9104145a2ff22be710158 100644 (file)
--- a/helm/software/components/ng_paramodulation/pp.ml
+++ b/helm/software/components/ng_paramodulation/pp.ml
@@ -88,18 +88,22 @@ let string_of_comparison = function
   | Terms.Invertible -> "=<->="
 
 let pp_literal ~formatter:f l =
-    match fst l with
-      | Terms.Predicate t ->
+    match l with
+      | Terms.Predicate t,sel ->
          Format.fprintf f "@[<hv>{";
+          if sel then Format.fprintf f "*";
          pp_foterm f t;
+          if sel then Format.fprintf f "*";
           Format.fprintf f "}@;"
-      | Terms.Equation (lhs, rhs, ty, comp) ->
+      | Terms.Equation (lhs, rhs, ty, comp),sel ->
          Format.fprintf f "@[<hv>{";
+          if sel then Format.fprintf f "*";
          pp_foterm f ty;
           Format.fprintf f "}:@;@[<hv>";
          pp_foterm f lhs;
           Format.fprintf f "@;%s@;" (string_of_comparison comp);
          pp_foterm f rhs;
+          if sel then Format.fprintf f "*";
           Format.fprintf f "@]@;"
 ;;