fixed infer_goal, added simplification before inferring with current

[helm.git] / helm / software / components / tactics / paramodulation / inference.mli

diff --git a/helm/software/components/tactics/paramodulation/inference.mli b/helm/software/components/tactics/paramodulation/inference.mli
index 9bfb84cb21f8ea7f0164845544ba556a02c51e0d..5c6a1979b5c4a38c0ebe3c6dab3d8ae181c59fac 100644 (file)
--- a/helm/software/components/tactics/paramodulation/inference.mli
+++ b/helm/software/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
 
 (**
@@ -75,3 +75,4 @@ val find_library_theorems:
 val find_context_hypotheses:
   Utils.environment -> int list -> (Cic.term * Cic.term * Cic.metasenv) list
 
+val get_stats: unit -> string