let rec first exc = function
| [] ->
raise (wrap_exc (lazy (localise orig_t, Printf.sprintf
- "The term %s has type %s but is here used with type %s"
+ "The term\n%s\nhas type\n%s\nbut is here used with type\n%s"
(NCicPp.ppterm ~metasenv ~subst ~context t)
(NCicPp.ppterm ~metasenv ~subst ~context infty)
(NCicPp.ppterm ~metasenv ~subst ~context expty))) exc)