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

diff --git a/helm/ocaml/tactics/tacticChaser.mli b/helm/ocaml/tactics/tacticChaser.mli
index 847dbc8b8..d54de4603 100644
--- a/helm/ocaml/tactics/tacticChaser.mli
+++ b/helm/ocaml/tactics/tacticChaser.mli
@@ -25,9 +25,8 @@
 
 val matchConclusion : MQIConn.handle ->
   ?output_html:(string -> unit) ->
-    (* boolean value: true = in main position *)
-  choose_must:((MQGTypes.uri * bool) list list ->
-               (MQGTypes.uri * bool) list ->
-               (MQGTypes.uri * bool) list) ->
+  choose_must:(MQGTypes.r_obj list list ->
+               MQGTypes.r_obj list ->
+               MQGTypes.r_obj list) ->
   unit -> status: ProofEngineTypes.status -> string list