X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Finference.mli;h=5c6a1979b5c4a38c0ebe3c6dab3d8ae181c59fac;hb=92081320b50b03d6bf296552d2cae9e4b398f1be;hp=9bfb84cb21f8ea7f0164845544ba556a02c51e0d;hpb=9559b53134624dbee523cf6406a9852665c0ff77;p=helm.git diff --git a/components/tactics/paramodulation/inference.mli b/components/tactics/paramodulation/inference.mli index 9bfb84cb2..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 (** @@ -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