From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 27 Jan 2004 17:29:18 +0000 (+0000)
Subject: use CicUtil.lookup_meta
X-Git-Tag: V_0_2_3~129
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b621ad609dab703c4a8055e2554fe39b1bcfb07c;p=helm.git

use CicUtil.lookup_meta
---

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 2ba10d742..b034e3928 100644
--- 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!!! *)