+ (fun (u,saturations,cpos) ->
+ let ty = type_uri u in
+ let src_name, tgt_name =
+ let rec aux ctx cpos t =
+ match cpos, t with
+ | 0,Cic.Prod (_,src,tgt) ->
+ CicPp.pp src ctx, tgt, (Some (Cic.Name "_")::ctx)
+ | 0,t -> CicPp.pp t ctx, Cic.Implicit None, []
+ | n,Cic.Prod (_,_,tgt) -> aux (Some (Cic.Name "_")::ctx) (n-1) tgt
+ | _ -> assert false
+ in
+ let ssrc, rest, ctx = aux [] cpos ty in
+ let stgt, rest, _ = aux ctx saturations rest in
+ let stgt =
+ if rest <> Cic.Implicit None then
+ match tgt with
+ | CoercDb.Fun _ -> CoercDb.string_of_carr tgt
+ | _ -> assert false
+ else
+ stgt
+ in
+ ssrc, stgt
+ in
+ Pp.node src_name fmt;
+ Pp.node tgt_name fmt;