- new generated query "unreferred" implemented at server side

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

diff --git a/helm/ocaml/tactics/tacticChaser.mli b/helm/ocaml/tactics/tacticChaser.mli
index f514360acc8a16a24ad6f96e937ecf21902ad457..d54de46037121ba7a4a876e3cc5431afa319ae18 100644 (file)
--- a/helm/ocaml/tactics/tacticChaser.mli
+++ b/helm/ocaml/tactics/tacticChaser.mli
@@ -23,11 +23,10 @@
  * 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.r_obj list list ->
+               MQGTypes.r_obj list ->
+               MQGTypes.r_obj list) ->
   unit -> status: ProofEngineTypes.status -> string list