X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Futils.mli;h=2f1533e69260638ca834789e2820ff46732bc4b2;hb=e8f64678cc425f19336ff4f905f9b2f00acd6627;hp=f44cab460ee5837043e07cfc29eb23a5f7d5fbe7;hpb=a060ed37101ce0e97bc26af8d49ce2491471c60c;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/utils.mli b/helm/software/components/tactics/paramodulation/utils.mli
index f44cab460..2f1533e69 100644
--- a/helm/software/components/tactics/paramodulation/utils.mli
+++ b/helm/software/components/tactics/paramodulation/utils.mli
@@ -87,6 +87,7 @@ val compute_equality_weight: Cic.term * Cic.term * Cic.term * comparison -> int
 
 val debug_print: string Lazy.t -> unit
 
+val eq_URI: unit -> UriManager.uri
 val eq_ind_URI: unit -> UriManager.uri
 val eq_ind_r_URI: unit -> UriManager.uri
 val sym_eq_URI: unit -> UriManager.uri