upgraded code to work with non-default equalities

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

diff --git a/helm/ocaml/paramodulation/utils.mli b/helm/ocaml/paramodulation/utils.mli
index 7814a4b88d3eed6c83e0f57d7e8ff0c0522155e2..910c4a651940d11e25afeb5b44539e8eb3c3af9d 100644 (file)
--- a/helm/ocaml/paramodulation/utils.mli
+++ b/helm/ocaml/paramodulation/utils.mli
@@ -45,3 +45,9 @@ val string_of_pos: pos -> string
 val compute_equality_weight: Cic.term -> Cic.term -> Cic.term -> int
 
 val debug_print: string Lazy.t -> unit
+
+val eq_ind_URI: unit -> UriManager.uri
+val eq_ind_r_URI: unit -> UriManager.uri
+val sym_eq_URI: unit -> UriManager.uri
+val eq_XURI: unit -> UriManager.uri
+val trans_eq_URI: unit -> UriManager.uri