X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Futils.ml;h=4a20f5c3d80eb1547d88801d88d4741c96965f9e;hb=8aaf525856e25bcd8f355e505fd00f45c62bc18f;hp=b0aa00e890021aa93d00a4e38340efe283697cab;hpb=92d100db14a01e3fb70a7d5151ac1e60d5a782a0;p=helm.git diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml index b0aa00e89..4a20f5c3d 100644 --- a/helm/ocaml/paramodulation/utils.ml +++ b/helm/ocaml/paramodulation/utils.ml @@ -397,3 +397,12 @@ let rec lpo t1 t2 = (* settable by the user... *) let compare_terms = ref nonrec_kbo;; + + +type equality_sign = Negative | Positive;; + +let string_of_sign = function + | Negative -> "Negative" + | Positive -> "Positive" +;; +