+ prerr_endline "#####";
+ let cobj = ("xxx", [], None, `Joint {
+ Content.joint_id = "yyy";
+ joint_kind = `Recursive [recno];
+ joint_defs =
+ [ `Definition {
+ Content.def_name = Some srec_name;
+ def_id = "zzz";
+ def_aref = "www";
+ def_term = bo;
+ def_type =
+ List.fold_right
+ (fun x t -> CicNotationPt.Binder(`Forall,x,t))
+ final_params cty
+ }
+ ];
+ })
+ in
+ let ids_to_nrefs = Hashtbl.create 1 in
+ let boxml = Content2pres.ncontent2pres ~ids_to_nrefs cobj in
+ prerr_endline (
+ (BoxPp.render_to_string ~map_unicode_to_tex:false
+ (function x::_ -> x | _ -> assert false) 80
+ (CicNotationPres.mpres_of_box boxml)));