metasenv,subst,(relevance,n,ty,cl)::res,(n,NCic.Decl ty)::ctx
) (metasenv,subst,[],[]) itl in
let metasenv,subst,itl,_ =
List.fold_left
(fun (metasenv,subst,res,i) (it_relev,n,ty,cl) ->
metasenv,subst,(relevance,n,ty,cl)::res,(n,NCic.Decl ty)::ctx
) (metasenv,subst,[],[]) itl in
let metasenv,subst,itl,_ =
List.fold_left
(fun (metasenv,subst,res,i) (it_relev,n,ty,cl) ->