moved string_of_equality into utils

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

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)
+    )
+;;
+
+

diff --git a/helm/ocaml/paramodulation/utils.mli b/helm/ocaml/paramodulation/utils.mli
index 471e6e307f654f37f24fd5949d55e8a266467f1d..164d4f303b8fde4cc44371ee9c7c7a9b977172cd 100644 (file)
--- a/helm/ocaml/paramodulation/utils.mli
+++ b/helm/ocaml/paramodulation/utils.mli
@@ -19,6 +19,9 @@ val compare_weights: ?normalize:bool -> weight -> weight -> comparison
 
 val nonrec_kbo: Cic.term -> Cic.term -> comparison
 
+val string_of_equality:
+  ?env:Inference.environment -> Inference.equality -> string
+
 val nonrec_kbo_w: (Cic.term * weight) -> (Cic.term * weight) -> comparison
 
 val names_of_context: Cic.context -> (Cic.name option) list