use CicUtil.lookup_meta

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 2ba10d7426926dcb1ccbd095ac3188394e6f4260..b034e3928800e139e80e94e7d2396618f8e66255 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -1348,9 +1348,7 @@ and type_of_aux' metasenv context t =
        decr fdebug ;
        ty
     | C.Meta (n,l) -> 
-       let (_,canonical_context,ty) =
-        List.find (function (m,_,_) -> n = m) metasenv
-       in
+       let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
         check_metasenv_consistency metasenv context canonical_context l;
         CicSubstitution.lift_meta l ty
     | C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)