moved string_of_equality into utils

[helm.git] / helm / ocaml / paramodulation / saturation.ml

diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml
index 405ba15a632307b773a22a1b68d20a1615344450..6508e75dac896900d9941f3a486685b7c463757b 100644 (file)
--- a/helm/ocaml/paramodulation/saturation.ml
+++ b/helm/ocaml/paramodulation/saturation.ml
@@ -15,24 +15,6 @@ let string_of_sign = function
 ;;
 
 
-let string_of_equality ?env =
-  match env with
-  | None -> (
-      function
-        | _, (ty, left, right), _, _ ->
-            Printf.sprintf "{%s}: %s = %s" (CicPp.ppterm ty)
-              (CicPp.ppterm left) (CicPp.ppterm right)
-    )
-  | Some (_, context, _) -> (
-      let names = names_of_context context in
-      function
-        | _, (ty, left, right), _, _ ->
-            Printf.sprintf "{%s}: %s = %s" (CicPp.pp ty names)
-              (CicPp.pp left names) (CicPp.pp right names)
-    )
-;;
-
-
 module OrderedEquality =
 struct
   type t = Inference.equality