split into two major parts:

[helm.git] / helm / ocaml / tactics / tacticChaser.ml

diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml
index f248735df91f609b36bc8e1ec44ee0004fd4390d..7270b70b3d5e0be8d09fe1a4f13e7d8a7518be9c 100644 (file)
--- a/helm/ocaml/tactics/tacticChaser.ml
+++ b/helm/ocaml/tactics/tacticChaser.ml
@@ -40,13 +40,13 @@ 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 (_, 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 result =
         I.execute mqi_handle 
            (G.query_of_constraints
-        (Some U.universe_for_match_conclusion)
+        (Some CGMatchConclusion.universe)
         (must,[],[]) (Some only,None,None)) in 
        let uris =
         List.map