moved string_of_equality into utils

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

diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml
index 01293a958c165b9fde5d6109ff90d09534f97dde..8d97e0c4bbb8ca198d2ecf9fb449527432edac13 100644 (file)
--- a/helm/ocaml/paramodulation/utils.ml
+++ b/helm/ocaml/paramodulation/utils.ml
@@ -287,3 +287,22 @@ let names_of_context context =
     context
 ;;
 
+
+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)
+    )
+;;
+
+