cambiato il tipo equality, aggiunto l'ordinamento tra left e right

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

diff --git a/helm/ocaml/paramodulation/utils.mli b/helm/ocaml/paramodulation/utils.mli
index 1adf90e5045094c048c30fe624f3d4ade8b2e068..295d1aa4d47d4c73ed428fd6ea26f0577ff2625f 100644 (file)
--- a/helm/ocaml/paramodulation/utils.mli
+++ b/helm/ocaml/paramodulation/utils.mli
@@ -31,3 +31,8 @@ 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
+