match coer with
| CoercGraph.NoCoercion
| CoercGraph.NotHandled _ ->
- let msg =
+ let msg e =
lazy ("The term " ^
CicMetaSubst.ppterm_in_context subst hete
context ^ " has type " ^
CicMetaSubst.ppterm_in_context subst hety
context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context subst s context)
+ CicMetaSubst.ppterm_in_context subst s context
+ (* "\nReason: " ^ Lazy.force e*))
in
- enrich (fun _ -> msg) exn
+ enrich msg exn
| CoercGraph.NotMetaClosed ->
raise (Uncertain (lazy "Coercions on meta"))
| CoercGraph.SomeCoercion c ->