X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FapplyTransformation.ml;h=4883deaf8665ba06816412cc121d04e5fdd7b323;hb=fbdd1cc46819d19ed135391a4a954c19d1b92c0c;hp=cff93ace3458413cf2e4089c36a9df3cde4d5709;hpb=4ee45a5645feb616089f64ba8902b3acfc72f728;p=helm.git

diff --git a/matita/applyTransformation.ml b/matita/applyTransformation.ml
index cff93ace3..4883deaf8 100644
--- a/matita/applyTransformation.ml
+++ b/matita/applyTransformation.ml
@@ -107,6 +107,7 @@ ignore (
   (fun ~metasenv subst term context ->
     try
      let context' = CicMetaSubst.apply_subst_context subst context in
+     let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
      let term' = CicMetaSubst.apply_subst subst term in
      let res = txt_of_cic_term 30 metasenv context' term' in
       if String.contains res '\n' then
@@ -179,7 +180,7 @@ let txt_of_cic_object ?map_unicode_to_tex n style prefix obj =
             (CicNotationPres.mpres_of_box bobj)
 	)
      | G.Procedural depth ->
-        let obj = ProceduralPreprocess.pp_obj obj in
+        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 (n - 8) ids_to_inner_sorts in
         let lazy_term_pp = term_pp in
@@ -187,7 +188,7 @@ let txt_of_cic_object ?map_unicode_to_tex n style prefix obj =
         let aux = GrafiteAstPp.pp_statement ~term_pp ~lazy_term_pp ~obj_pp in
 	let script = Acic2Procedural.acic2procedural 
 	   ~ids_to_inner_sorts ~ids_to_inner_types ?depth prefix aobj in
-	"\n" ^ String.concat "" (List.map aux script)
+	String.concat "" (List.map aux script) ^ "\n\n"
 
 let txt_of_inline_macro style suri prefix =
    let dbd = LibraryDb.instance () in