X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Finference.mli;h=55f3df414aa7949e0f8c7bc08cb368da216d7d4a;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=f2b7073d1378314e122be29fa5143324b0521093;hpb=b6bec181b81b3cbc56ec8914dcd7e6a029c7d84f;p=helm.git

diff --git a/helm/ocaml/paramodulation/inference.mli b/helm/ocaml/paramodulation/inference.mli
index f2b7073d1..55f3df414 100644
--- a/helm/ocaml/paramodulation/inference.mli
+++ b/helm/ocaml/paramodulation/inference.mli
@@ -84,7 +84,7 @@ val find_equalities:
 *)
 val find_library_equalities:
   HMysql.dbd -> Cic.context -> ProofEngineTypes.status -> int ->
-  UriManager.UriSet.t * equality list * int
+  UriManager.UriSet.t * (UriManager.uri * equality) list * int
 
 (**
    searches the library for theorems that are not equalities (returned by the