" is not a sort: " ^ status#ppterm ~metasenv ~subst ~context ty)) in
let ty = NCicReduction.whd status ~subst context ty in
let exn =
" is not a sort: " ^ status#ppterm ~metasenv ~subst ~context ty)) in
let ty = NCicReduction.whd status ~subst context ty in
let exn =