fixed LApply pretty printing

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

diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml
index b0aa00e890021aa93d00a4e38340efe283697cab..f2c475799cf818e2aebec504efd2af369823d53e 100644 (file)
--- a/helm/ocaml/paramodulation/utils.ml
+++ b/helm/ocaml/paramodulation/utils.ml
@@ -397,3 +397,19 @@ 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"
+;;
+
+
+type pos = Left | Right 
+
+let string_of_pos = function
+  | Left -> "Left"
+  | Right -> "Right"
+;;