first moogle template checkin

[helm.git] / helm / ocaml / tactics / tacticChaser.mli

diff --git a/helm/ocaml/tactics/tacticChaser.mli b/helm/ocaml/tactics/tacticChaser.mli
index d54de46037121ba7a4a876e3cc5431afa319ae18..d4f8a2c540402273b79173416dfab3439b186cc8 100644 (file)
--- a/helm/ocaml/tactics/tacticChaser.mli
+++ b/helm/ocaml/tactics/tacticChaser.mli
@@ -28,5 +28,14 @@ val matchConclusion : MQIConn.handle ->
   choose_must:(MQGTypes.r_obj list list ->
                MQGTypes.r_obj list ->
                MQGTypes.r_obj list) ->
-  unit -> status: ProofEngineTypes.status -> string list
+  unit -> ProofEngineTypes.status -> string list
+
+
+(* TODO: OLD CODE TO BE REMOVED
+val searchTheorem : ProofEngineTypes.status -> ProofEngineTypes.proof * ProofEngineTypes.goal list
+*)
+
+val searchTheorems:
+  MQIConn.handle -> ProofEngineTypes.status ->
+    (ProofEngineTypes.proof * ProofEngineTypes.goal list) list