X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FtacticChaser.ml;h=06333d2316582b4615dc4a3618536643539752a5;hb=e7e2a523299d807370b292b44e77f46fad1638c9;hp=6f83c3fd67bb726d95fae43fe24e8fbada6b1f52;hpb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;p=helm.git

diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml
index 6f83c3fd6..06333d231 100644
--- a/helm/ocaml/tactics/tacticChaser.ml
+++ b/helm/ocaml/tactics/tacticChaser.ml
@@ -33,27 +33,21 @@
 (*                                                                            *)
 (******************************************************************************)
 
+module I = MQueryInterpreter
+module U = MQGUtil
+module G = MQueryGenerator
+
   (* search arguments on which Apply tactic doesn't fail *)
-let searchPattern mqi_handle ?(output_html = (fun _ -> ())) ~choose_must () ~status =
+let matchConclusion 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
+  let list_of_must, only = CGMatchConclusion.get_constraints metasenv ey ty in
   let must = choose_must list_of_must only in
-  let torigth_restriction (u,b) =
-   let p =
-    if b then
-     "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion" 
-    else
-     "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion"
-    in
-    (u,p,None)
-  in
-  let rigth_must = List.map torigth_restriction must in
-  let rigth_only = Some (List.map torigth_restriction only) in
   let result =
-	 MQueryInterpreter.execute mqi_handle 
-	    (MQueryGenerator.query_of_constraints None
-		(rigth_must,[],[]) (rigth_only,None,None)) in 
+	 I.execute mqi_handle 
+	    (G.query_of_constraints
+        (Some CGMatchConclusion.universe)
+        (must,[],[]) (Some only,None,None)) in 
 	let uris =
 	 List.map
 		(function uri,_ ->