Content2pres.content2pres
?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_inner_sorts cobj
in
- remove_closed_substs ("\n\n" ^
+ remove_closed_substs (
BoxPp.render_to_string ~map_unicode_to_tex
(function _::x::_ -> x | _ -> assert false) n
(CicNotationPres.mpres_of_box bobj)
- )
+ ^ "\n\n" )
| G.Procedural depth ->
(*
PO.critical := false;