X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Feta_fixing.ml;h=29d22ccb91062051858e1c55f4619b4433e35e35;hb=refs%2Ftags%2FPRE_UNIVERSES;hp=167244c280040130986885566ab30c27b672f6f6;hpb=1fb8d0192e1f7ee891c53dc282c9c9f111e63e3c;p=helm.git diff --git a/helm/ocaml/cic_omdoc/eta_fixing.ml b/helm/ocaml/cic_omdoc/eta_fixing.ml index 167244c28..29d22ccb9 100644 --- a/helm/ocaml/cic_omdoc/eta_fixing.ml +++ b/helm/ocaml/cic_omdoc/eta_fixing.ml @@ -177,10 +177,8 @@ let eta_fix metasenv context t = let exp_named_subst' = fix_exp_named_subst context exp_named_subst in C.Var (uri,exp_named_subst') | C.Meta (n,l) -> - let (_,canonical_context,_) = - List.find (function (m,_,_) -> n = m) metasenv - in - let l' = + let (_,canonical_context,_) = CicUtil.lookup_meta n metasenv in + let l' = List.map2 (fun ct t -> match (ct, t) with