ocaml 3.09 transition

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

diff --git a/helm/ocaml/paramodulation/inference.mli b/helm/ocaml/paramodulation/inference.mli
index f2b7073d1378314e122be29fa5143324b0521093..55f3df414aa7949e0f8c7bc08cb368da216d7d4a 100644 (file)
--- 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