]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/tactics/tacticChaser.ml
MQueryInterpreter: interface updated
[helm.git] / helm / ocaml / tactics / tacticChaser.ml
index d09eacc49773a2a655db35a2d545e47c5a9bb975..47adfeee5ed487ef951ca97cc642b2b1be380c25 100644 (file)
@@ -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