in
metasenv, subst, t, infty
| C.Sort s ->
- (try metasenv, subst, t, C.Sort (NCicEnvironment.typeof_sort s)
+ (try metasenv, subst, t, C.Sort (NCicEnvironment.typeof_sort status s)
with
| NCicEnvironment.UntypableSort msg ->
raise (RefineFailure (lazy (localise t, Lazy.force msg)))
let ty = NCicReduction.whd status ~subst context ty in
try_coercions status ~localise metasenv subst context
t orig_t ty (NCic.Sort (NCic.Type
- (match NCicEnvironment.get_universes () with
+ (match NCicEnvironment.get_universes status with
| x::_ -> x
| _ -> assert false))) false
(Uncertain (lazy (localise orig_t,
NCicReduction.whd status ~subst [] ty_sort
with
(C.Sort (C.Type u1) as s1), (C.Sort (C.Type u2) as s2) ->
- if not (NCicEnvironment.universe_leq u1 u2) then
+ if not (NCicEnvironment.universe_leq status u1 u2) then
raise
(RefineFailure
(lazy(localise te, "The type " ^