X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FtacticChaser.mli;h=847dbc8b8942ee3e4a33492d8f62cd83c9590b67;hb=0e74e8e94eada756157addce67e4adeb8dff1feb;hp=f514360acc8a16a24ad6f96e937ecf21902ad457;hpb=65e3c9976212e04a4678ff9ce9e3c2f436d06d33;p=helm.git

diff --git a/helm/ocaml/tactics/tacticChaser.mli b/helm/ocaml/tactics/tacticChaser.mli
index f514360ac..847dbc8b8 100644
--- a/helm/ocaml/tactics/tacticChaser.mli
+++ b/helm/ocaml/tactics/tacticChaser.mli
@@ -23,11 +23,11 @@
  * 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) ->
+  choose_must:((MQGTypes.uri * bool) list list ->
+               (MQGTypes.uri * bool) list ->
+               (MQGTypes.uri * bool) list) ->
   unit -> status: ProofEngineTypes.status -> string list