~subst metasenv context t CicUniv.oblivion_ugraph
in
let bag, head, metasenv, args =
- Equality.saturate_term bag metasenv context ty
+ Equality.saturate_term bag metasenv subst context ty
in
let mes = CicUtil.metas_of_term (Cic.Appl (head::t::args)) in
let t = if args = [] then t else Cic.Appl (t:: args) in