X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FtacticChaser.mli;h=e7e63954a7d667d629ae420d365f068e62f30bc4;hb=2bd307bda75f4aee3b95c3d5039c64b34408dc6c;hp=d54de46037121ba7a4a876e3cc5431afa319ae18;hpb=96134b9ec1030ed15cea00d751dd4d744463f62c;p=helm.git

diff --git a/helm/ocaml/tactics/tacticChaser.mli b/helm/ocaml/tactics/tacticChaser.mli
index d54de4603..e7e63954a 100644
--- a/helm/ocaml/tactics/tacticChaser.mli
+++ b/helm/ocaml/tactics/tacticChaser.mli
@@ -30,3 +30,11 @@ val matchConclusion : MQIConn.handle ->
                MQGTypes.r_obj list) ->
   unit -> status: ProofEngineTypes.status -> string list
 
+
+(* TODO: OLD CODE TO BE REMOVED
+val searchTheorem : status: ProofEngineTypes.status -> ProofEngineTypes.proof * ProofEngineTypes.goal list
+*)
+
+val searchTheorems : MQIConn.handle -> status: ProofEngineTypes.status -> (ProofEngineTypes.proof * ProofEngineTypes.goal list) list
+
+