From b621ad609dab703c4a8055e2554fe39b1bcfb07c Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 27 Jan 2004 17:29:18 +0000 Subject: [PATCH] use CicUtil.lookup_meta --- helm/ocaml/cic_proof_checking/cicTypeChecker.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) 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!!! *) -- 2.39.2