X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FtacticChaser.ml;h=47adfeee5ed487ef951ca97cc642b2b1be380c25;hb=09151f33b14507e4d20380f3100a6db5f49f3f46;hp=d09eacc49773a2a655db35a2d545e47c5a9bb975;hpb=28f262128cd08dfaad435f73d3f4eee5976993d6;p=helm.git

diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml
index d09eacc49..47adfeee5 100644
--- a/helm/ocaml/tactics/tacticChaser.ml
+++ b/helm/ocaml/tactics/tacticChaser.ml
@@ -34,7 +34,7 @@
 (******************************************************************************)
 
   (* search arguments on which Apply tactic doesn't fail *)
-let searchPattern ?(output_html = (fun _ -> ())) ~choose_must () ~status =
+let searchPattern mqi_handle ?(output_html = (fun _ -> ())) ~choose_must () ~status =
  let ((_, metasenv, _, _), metano) = status in
  let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in
   let list_of_must,only = MQueryLevels.out_restr metasenv ey ty in
@@ -51,7 +51,7 @@ let searchPattern ?(output_html = (fun _ -> ())) ~choose_must () ~status =
   let rigth_must = List.map torigth_restriction must in
   let rigth_only = Some (List.map torigth_restriction only) in
   let result =
-	 MQueryGenerator.searchPattern
+	 MQueryGenerator.searchPattern mqi_handle
 		(rigth_must,[],[]) (rigth_only,None,None) in 
 	let uris =
 	 List.map