X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FtacticChaser.ml;h=7270b70b3d5e0be8d09fe1a4f13e7d8a7518be9c;hb=b38de2d3fa8bbe346c59c18bbeb889f29e493f63;hp=06333d2316582b4615dc4a3618536643539752a5;hpb=506b4b7597021c98e34fb65cf9d0bb7879f06e92;p=helm.git

diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml
index 06333d231..7270b70b3 100644
--- a/helm/ocaml/tactics/tacticChaser.ml
+++ b/helm/ocaml/tactics/tacticChaser.ml
@@ -40,7 +40,7 @@ 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 =