(* we try with a coercion *)
let rec first exc = function
| [] ->
+ let expty =
+ match expty with
+ `Type expty -> status#ppterm ~metasenv ~subst ~context expty
+ | `Sort -> "[[sort]]"
+ | `Prod -> "[[prod]]" in
pp (lazy "WWW: no more coercions!");
raise (wrap_exc (lazy (localise orig_t, Printf.sprintf
"The term\n%s\nhas type\n%s\nbut is here used with type\n%s"
`Type expty -> expty
| `Sort ->
NCic.Sort (NCic.Type
- (match NCicEnvironment.get_universes () with
+ (match NCicEnvironment.get_universes status with
| x::_ -> x
| _ -> assert false))
| `Prod -> NCic.Prod ("_",NCic.Implicit `Type,NCic.Implicit `Type)
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 " ^