X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fpp.ml;h=ddf5726c49d0f6b479958a4e48ca9f969440f30d;hb=f9abd21eb0d26cf9b632af4df819225be4d091e3;hp=625de5c31994b08f8b6fc0c08a85c5b1c620584a;hpb=772def9075b7b62870ebf4cecec6bcd37a549b1d;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/pp.ml b/helm/software/components/ng_paramodulation/pp.ml
index 625de5c31..ddf5726c4 100644
--- a/helm/software/components/ng_paramodulation/pp.ml
+++ b/helm/software/components/ng_paramodulation/pp.ml
@@ -85,6 +85,7 @@ let string_of_comparison = function
   | Terms.Gt -> "=>="
   | Terms.Eq -> "==="
   | Terms.Incomparable -> "=?="
+  | Terms.Invertible -> "=<->="
 
 let pp_unit_clause ~formatter:f c =
   let (id, l, vars, proof) = c in