upgraded code to work with non-default equalities

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

diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml
index 2d5ee24ce7612527102a3f128c586fa66511145d..27934674808bf339ec9c797c00de0375786da493 100644 (file)
--- a/helm/ocaml/paramodulation/utils.ml
+++ b/helm/ocaml/paramodulation/utils.ml
@@ -513,3 +513,12 @@ let string_of_pos = function
   | Left -> "Left"
   | Right -> "Right"
 ;;
+
+
+let eq_ind_URI () = LibraryObjects.eq_ind_URI ~eq:(LibraryObjects.eq_URI ())
+let eq_ind_r_URI () = LibraryObjects.eq_ind_r_URI ~eq:(LibraryObjects.eq_URI ())
+let sym_eq_URI () = LibraryObjects.sym_eq_URI ~eq:(LibraryObjects.eq_URI ())
+let eq_XURI () =
+  let s = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in
+  UriManager.uri_of_string (s ^ "#xpointer(1/1/1)")
+let trans_eq_URI () = LibraryObjects.trans_eq_URI ~eq:(LibraryObjects.eq_URI ())