(* 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
+ raise (wrap_exc (lazy
+ let expty =
+ match expty with
+ `Type expty -> status#ppterm ~metasenv ~subst ~context expty
+ | `Sort -> "[[sort]]"
+ | `Prod -> "[[prod]]" in
+ (localise orig_t, Printf.sprintf
"The term\n%s\nhas type\n%s\nbut is here used with type\n%s"
(status#ppterm ~metasenv ~subst ~context t)
(status#ppterm ~metasenv ~subst ~context infty)
metasenv, subst, t, ty
with
Failure _ ->
+ let msg =
+ (lazy (localise orig_t,
+ "The type of " ^ status#ppterm ~metasenv ~subst ~context t ^
+ " is not a sort: " ^ status#ppterm ~metasenv ~subst ~context ty)) in
let ty = NCicReduction.whd status ~subst context ty in
+ let exn =
+ if NCicUnification.could_reduce status ~subst context ty then
+ Uncertain msg
+ else
+ RefineFailure msg
+ in
try_coercions status ~localise metasenv subst context
- t orig_t ty `Sort
- (Uncertain (lazy (localise orig_t,
- "The type of " ^ status#ppterm ~metasenv ~subst ~context t ^
- " is not a sort: " ^ status#ppterm ~metasenv ~subst ~context ty)))
+ t orig_t ty `Sort exn
and sort_of_prod status localise metasenv subst context orig_s orig_t (name,s)
t (t1, t2)