X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2FapplyTransformation.ml;h=4ef0a5573be2b569375543e66f4c850e826f6067;hb=d6a96d7ae2a320e390ce60b0ee30feebf9f2ee28;hp=de87d55489c1ce31ef855550301a976c08c1c68f;hpb=94cf8189445df1c0ae1d406cd92c4c3ad866fc7e;p=helm.git

diff --git a/matita/applyTransformation.ml b/matita/applyTransformation.ml
index de87d5548..4ef0a5573 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
@@ -187,9 +188,14 @@ 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 print_exc = function
+      | ProofEngineHelpers.Bad_pattern s as e ->
+           Printexc.to_string e ^ " " ^ Lazy.force s
+      | e -> Printexc.to_string e
+   in
    let dbd = LibraryDb.instance () in   
    let sorted_uris = MetadataDeps.sorted_uris_of_baseuri ~dbd suri in
    let map uri =
@@ -198,6 +204,6 @@ let txt_of_inline_macro style suri prefix =
       with
          | e -> 
 	    Printf.sprintf "\n(* ERRORE IN STAMPA DI %s\nEXCEPTION: %s *)\n" 
-	    (UriManager.string_of_uri uri) (Printexc.to_string e)
+	    (UriManager.string_of_uri uri) (print_exc e)
    in
    String.concat "" (List.map map sorted_uris)