- | C.Sort (C.Type [false,u]) -> C.Sort (C.Type [true, 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))