with Failure _ ->
raise (TypeCheckerFailure (lazy ("unbound variable " ^ string_of_int n
^" under: " ^ NCicPp.ppcontext ~metasenv ~subst context))))
- | C.Sort (C.Type [false,u]) -> C.Sort (C.Type [true, u])
+ | C.Sort (C.Type ([false,u] as univ)) ->
+ if NCicEnvironment.is_declared univ then
+ C.Sort (C.Type [true, u])
+ else
+ raise (TypeCheckerFailure (lazy ("undeclared universe " ^
+ NUri.string_of_uri u)))
| C.Sort (C.Type _) ->
raise (AssertFailure (lazy ("Cannot type an inferred type: "^
NCicPp.ppterm ~subst ~metasenv ~context t)))