X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FtacticChaser.mli;h=d4f8a2c540402273b79173416dfab3439b186cc8;hb=3bb4ce11fb9d4c6375483a80344beb94c4517dd7;hp=f514360acc8a16a24ad6f96e937ecf21902ad457;hpb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;p=helm.git

diff --git a/helm/ocaml/tactics/tacticChaser.mli b/helm/ocaml/tactics/tacticChaser.mli
index f514360ac..d4f8a2c54 100644
--- a/helm/ocaml/tactics/tacticChaser.mli
+++ b/helm/ocaml/tactics/tacticChaser.mli
@@ -23,11 +23,19 @@
  * http://cs.unibo.it/helm/.
  *)
 
-val searchPattern : MQIConn.handle ->
+val matchConclusion : MQIConn.handle ->
   ?output_html:(string -> unit) ->
-    (* boolean value: true = in main position *)
-  choose_must:((MQueryGenerator.uri * bool) list list ->
-               (MQueryGenerator.uri * bool) list ->
-               (MQueryGenerator.uri * bool) list) ->
-  unit -> status: ProofEngineTypes.status -> string list
+  choose_must:(MQGTypes.r_obj list list ->
+               MQGTypes.r_obj list ->
+               MQGTypes.r_obj 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