From: Alberto Griggio <griggio@fbk.eu>
Date: Fri, 13 May 2005 09:05:27 +0000 (+0000)
Subject: moved string_of_equality into utils
X-Git-Tag: single_binding~79
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6cce91267c785d7790e9377717a13d0546bb68e1;p=helm.git

moved string_of_equality into utils
---

diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml
index 405ba15a6..6508e75da 100644
--- 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 01293a958..8d97e0c4b 100644
--- 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 471e6e307..164d4f303 100644
--- 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