fixed a bug (status not reset properly between calls), tried some other

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

diff --git a/helm/ocaml/paramodulation/inference.mli b/helm/ocaml/paramodulation/inference.mli
index 560af55da9af9a438b2f086fe7a4aa722949857c..1d76aba7a8495d0ca91838e53b5ad55b4e93b94d 100644 (file)
--- a/helm/ocaml/paramodulation/inference.mli
+++ b/helm/ocaml/paramodulation/inference.mli
@@ -112,7 +112,7 @@ val find_library_equalities:
 
 val find_library_theorems:
   HMysql.dbd -> environment -> ProofEngineTypes.status -> UriManager.UriSet.t ->
-  (Cic.term * Cic.term * Cic.metasenv) list
+  (UriManager.uri * Cic.term * Cic.term * Cic.metasenv) list
 
 val find_context_hypotheses:
   environment -> int list -> (Cic.term * Cic.term * Cic.metasenv) list