X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fpp.ml;fp=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fpp.ml;h=5008489df828b48c95b9104145a2ff22be710158;hb=b714e87e96f14f332a5157567a4c62a4b28fa8eb;hp=d93fade272e9479be851a5dbb33853f6d26ecf8e;hpb=ddba563cd3f42a7947a0e0b464d5dd3c5f9b299d;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/pp.ml b/helm/software/components/ng_paramodulation/pp.ml
index d93fade27..5008489df 100644
--- 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 "@]@;"
 ;;