let ty = NCicReduction.whd status ~subst context ty in
try_coercions status ~localise metasenv subst context
t orig_t ty (NCic.Sort (NCic.Type
let ty = NCicReduction.whd status ~subst context ty in
try_coercions status ~localise metasenv subst context
t orig_t ty (NCic.Sort (NCic.Type