| SomeCoercion of Cic.term
| NoCoercion
| NotMetaClosed
- | NotHandled of string
+ | NotHandled of string Lazy.t
let debug = false
let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
CicTypeChecker.type_of_aux' [] [] c univ
with CicTypeChecker.TypeCheckerFailure s as exn ->
debug_print (lazy (sprintf "Generated composite coercion:\n%s\n%s"
- (CicPp.ppterm c) s));
+ (CicPp.ppterm c) (Lazy.force s)));
raise exn
in
let cleaned_ty =