- | C.Sort (C.Type [false,u]) -> metasenv,subst,t,(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 _ -> metasenv,subst,t,(C.Sort (C.Type NCicEnvironment.type0))
+ | C.Sort s ->
+ (try metasenv, subst, t, C.Sort (NCicEnvironment.typeof_sort s)
+ with
+ | NCicEnvironment.UntypableSort msg ->
+ raise (RefineFailure (lazy (localise t, Lazy.force msg)))
+ | NCicEnvironment.AssertFailure msg -> raise (AssertFailure msg))