+let pp_hint t p =
+ let context, t =
+ let rec aux ctx = function
+ | NCic.Prod (name, ty, rest) -> aux ((name, NCic.Decl ty) :: ctx) rest
+ | t -> ctx, t
+ in
+ aux [] t
+ in
+ let recproblems, concl =
+ let rec aux ctx = function
+ | NCic.LetIn (name,ty,bo,rest) -> aux ((name, NCic.Def(bo,ty))::ctx) rest
+ | t -> ctx, t
+ in
+ aux [] t
+ in
+ let buff = Buffer.create 100 in
+ let fmt = Format.formatter_of_buffer buff in
+(*
+ F.fprintf "@[<hov>"
+ F.fprintf "@[<hov>"
+(* pp_ctx [] context *)
+ F.fprintf "@]"
+ F.fprintf "@;"
+ F.fprintf "@[<hov>"
+(* pp_ctx context recproblems *)
+ F.fprintf "@]"
+ F.fprintf "\vdash@;";
+ NCicPp.ppterm ~fmt ~context:(recproblems@context) ~subst:[] ~metasenv:[];
+ F.fprintf "@]"
+ F.fprintf formatter "@?";
+ prerr_endline (Buffer.contents buff);
+*)
+()
+;;