- BoxPp.render_to_string (function _::x::_ -> x | _ -> assert false) n (CicNotationPres.mpres_of_box bobj)
- )
- | GrafiteAst.Procedural depth ->
- let term_pp = term2pres (n - 8) ids_to_inner_sorts in
+ BoxPp.render_to_string ~map_unicode_to_tex
+ (function _::x::_ -> x | _ -> assert false) n
+ (CicNotationPres.mpres_of_box bobj)
+ )
+ | G.Procedural depth ->
+ let obj = ProceduralOptimizer.optimize_obj obj in
+ let aobj, ids_to_inner_sorts, ids_to_inner_types = get_aobj obj in
+ let term_pp = term2pres ~map_unicode_to_tex (n - 8) ids_to_inner_sorts in