X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Finference.mli;h=0de5e8433a6a9db6f885609927293df0b1952021;hb=e8f64678cc425f19336ff4f905f9b2f00acd6627;hp=9bfb84cb21f8ea7f0164845544ba556a02c51e0d;hpb=5b911ecf8bcb1644b82316d5f2709ae253a6a36d;p=helm.git diff --git a/helm/software/components/tactics/paramodulation/inference.mli b/helm/software/components/tactics/paramodulation/inference.mli index 9bfb84cb2..0de5e8433 100644 --- a/helm/software/components/tactics/paramodulation/inference.mli +++ b/helm/software/components/tactics/paramodulation/inference.mli @@ -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