Fixed conflicts due to problem when merging with UEQ implementation

[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 625de5c31994b08f8b6fc0c08a85c5b1c620584a..ddf5726c49d0f6b479958a4e48ca9f969440f30d 100644 (file)
--- 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