]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/applyTransformation.ml
- MatitaMisc: we factorized here the function out_preamble used in matitadep
[helm.git] / helm / software / matita / applyTransformation.ml
index c504996e0d225e18ebe89e83e0188e680a0994eb..21b841f4165f90586f396eb9955124e52a2a3854 100644 (file)
@@ -205,11 +205,11 @@ let txt_of_cic_object
           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;