- let xet = match get_inner_types st t with
- | Some (_, et) -> Some (cic et)
- | None -> None
+ let xtypes, note = match get_inner_types st t with
+ | Some (it, et) -> Some (H.cic it, H.cic et),
+ (Printf.sprintf "\nInferred: %s\nExpected: %s"
+ (Pp.ppterm (H.cic it)) (Pp.ppterm (H.cic et)))
+ | None -> None, "\nNo types"