+ (prerr_endline ("entro");
+ let p =
+ (acic2content seed ?name:(name_of n) ~ids_to_inner_sorts ~ids_to_inner_types t)
+ in
+ (match p.K.proof_name with
+ Some "w" -> prerr_endline ("TUTTO BENE:");
+ | Some s -> prerr_endline ("mi chiamo " ^ s);
+ | _ -> prerr_endline ("ho perso il nome"););
+ prerr_endline ("esco"); `Proof p;)