X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FintroductionTactics.ml;h=b425f219af8585778f7b1a1bcc27fd57c774be39;hb=5a9b1f46a8e866382a71d686e689e9e5907f1824;hp=6318f489041d48e02e9590c501c53ff1a9e5cee1;hpb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;p=helm.git

diff --git a/helm/ocaml/tactics/introductionTactics.ml b/helm/ocaml/tactics/introductionTactics.ml
index 6318f4890..b425f219a 100644
--- a/helm/ocaml/tactics/introductionTactics.ml
+++ b/helm/ocaml/tactics/introductionTactics.ml
@@ -28,7 +28,7 @@ let constructor_tac ~n ~status:(proof, goal) =
   let module C = Cic in
   let module R = CicReduction in
    let (_,metasenv,_,_) = proof in
-    let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
      match (R.whd context ty) with
         (C.MutInd (uri, typeno, exp_named_subst))
       | (C.Appl ((C.MutInd (uri, typeno, exp_named_subst))::_)) ->