- | 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)))
- | C.Sort _ -> C.Sort (C.Type NCicEnvironment.type0)
+ | C.Sort s ->
+ (try C.Sort (NCicEnvironment.typeof_sort s)
+ with
+ | NCicEnvironment.UntypableSort msg -> raise (TypeCheckerFailure msg)
+ | NCicEnvironment.AssertFailure msg -> raise (AssertFailure msg))