+let pp_candidate context x = pp context (Lazy.force x)
+let pp_candidate_tip context x = pp ~size:0 context (Lazy.force x)
+let pp_candidate_type context x =
+ try
+ let ty, _ =
+ CicTypeChecker.type_of_aux' [] ~subst:[]
+ context (Lazy.force x) CicUniv.oblivion_ugraph
+ in
+ pp ~size:0 context ty
+ with CicUtil.Meta_not_found _ -> pp ~size:0 context (Lazy.force x)
+;;