X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Finference.mli;h=5c6a1979b5c4a38c0ebe3c6dab3d8ae181c59fac;hb=245c8538406d49df459efb1fe9d87474db4bd332;hp=0de5e8433a6a9db6f885609927293df0b1952021;hpb=356f9fafa095801f1be70ff495f0977ce96ed6bc;p=helm.git

diff --git a/components/tactics/paramodulation/inference.mli b/components/tactics/paramodulation/inference.mli
index 0de5e8433..5c6a1979b 100644
--- a/components/tactics/paramodulation/inference.mli
+++ b/components/tactics/paramodulation/inference.mli
@@ -57,7 +57,7 @@ val find_equalities:
    searches the library for equalities that can be applied to the current goal
 *)
 val find_library_equalities:
-  HMysql.dbd -> Cic.context -> ProofEngineTypes.status -> int ->
+  bool -> HMysql.dbd -> Cic.context -> ProofEngineTypes.status -> int ->
     UriManager.UriSet.t * (UriManager.uri * Equality.equality) list * int
 
 (**