X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Futils.ml;h=52d99327e8b5d284c143f57f864027026aa71b53;hb=6cf15c86b051582032c794f7da8a325e31fc0480;hp=b0aa00e890021aa93d00a4e38340efe283697cab;hpb=92d100db14a01e3fb70a7d5151ac1e60d5a782a0;p=helm.git

diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml
index b0aa00e89..52d99327e 100644
--- a/helm/ocaml/paramodulation/utils.ml
+++ b/helm/ocaml/paramodulation/utils.ml
@@ -7,8 +7,8 @@ let print_metasenv metasenv =
 ;;
 
 
-let print_subst subst =
-  String.concat "\n"
+let print_subst ?(prefix="\n") subst =
+  String.concat prefix
     (List.map
        (fun (i, (c, t, ty)) ->
           Printf.sprintf "?%d -> %s : %s" i
@@ -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"
+;;