X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Futils.mli;h=71f2fc1b5d5a3adee6f1d2634784b2c3797bb9f1;hb=cb7af66937e8c72ae6ea6694350a0c86f3e6ccf9;hp=1adf90e5045094c048c30fe624f3d4ade8b2e068;hpb=92d100db14a01e3fb70a7d5151ac1e60d5a782a0;p=helm.git

diff --git a/helm/ocaml/paramodulation/utils.mli b/helm/ocaml/paramodulation/utils.mli
index 1adf90e50..71f2fc1b5 100644
--- a/helm/ocaml/paramodulation/utils.mli
+++ b/helm/ocaml/paramodulation/utils.mli
@@ -31,3 +31,11 @@ val lpo: Cic.term -> Cic.term -> comparison
 
 (** term-ordering function settable by the user *)
 val compare_terms: (Cic.term -> Cic.term -> comparison) ref
+
+type equality_sign = Negative | Positive
+
+val string_of_sign: equality_sign -> string
+
+type pos = Left | Right 
+
+val string_of_pos: pos -> string