X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FtacticChaser.ml;h=7270b70b3d5e0be8d09fe1a4f13e7d8a7518be9c;hb=d3c72d6856cd185e5b3e9f2e8b928b78c7031ed1;hp=c4bfc5e034f17b170a387e28216a92556f0febd6;hpb=0e74e8e94eada756157addce67e4adeb8dff1feb;p=helm.git

diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml
index c4bfc5e03..7270b70b3 100644
--- a/helm/ocaml/tactics/tacticChaser.ml
+++ b/helm/ocaml/tactics/tacticChaser.ml
@@ -40,19 +40,14 @@ module G = MQueryGenerator
   (* search arguments on which Apply tactic doesn't fail *)
 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 (_, ey ,ty) = CicUtil.lookup_meta metano metasenv 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) =
-   (if b then `MainConclusion None else `InConclusion), u
-  in
-  let rigth_must = List.map torigth_restriction must in
-  let rigth_only = Some (List.map torigth_restriction only) in
   let result =
 	 I.execute mqi_handle 
 	    (G.query_of_constraints
-        (Some U.universe_for_match_conclusion)
-        (rigth_must,[],[]) (rigth_only,None,None)) in 
+        (Some CGMatchConclusion.universe)
+        (must,[],[]) (Some only,None,None)) in 
 	let uris =
 	 List.map
 		(function uri,_ ->