X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FapplyTransformation.ml;h=e741ed70c4ba8c79f1f88488057bd51522487b27;hb=0080faad4e730c227b6bbb2549407b23703b477a;hp=e1821ed88a2861147c0e4ffe7b544017dccdd280;hpb=75de1f4c87166f120d8bb42d98926adaf407c98c;p=helm.git

diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml
index e1821ed88..e741ed70c 100644
--- a/helm/software/matita/applyTransformation.ml
+++ b/helm/software/matita/applyTransformation.ml
@@ -44,6 +44,7 @@ module G  = GrafiteAst
 module GE = GrafiteEngine
 module LS = LibrarySync
 module Ds = CicDischarge
+module PO = ProceduralOptimizer
 
 let mpres_document pres_box =
   Xml.add_xml_declaration (CicNotationPres.print_box pres_box)
@@ -203,7 +204,7 @@ let txt_of_cic_object
             (CicNotationPres.mpres_of_box bobj)
         )
      | G.Procedural depth ->
-	let obj = ProceduralOptimizer.optimize_obj obj in
+	let obj, info = PO.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
         let lazy_term_pp = term_pp in
@@ -212,7 +213,7 @@ let txt_of_cic_object
          ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp in
         let script = 
            Acic2Procedural.procedural_of_acic_object 
-              ~ids_to_inner_sorts ~ids_to_inner_types 
+              ~ids_to_inner_sorts ~ids_to_inner_types ~info
 	      ?depth ?flavour prefix aobj 
   in
         "\n\n" ^ String.concat "" (List.map aux script)
@@ -279,7 +280,7 @@ let txt_of_inline_uri ~map_unicode_to_tex style ?flavour prefix suri =
 	in
 	if real then do_it obj else
 	let newuri = discharge_uri style uri in
-	let _lemmas = LS.add_obj GE.refinement_toolkit newuri obj in
+	let _lemmas = LS.add_obj ~pack_coercion_obj:CicRefine.pack_coercion_obj newuri obj in
 	do_it obj
       with
          | TC.TypeCheckerFailure s ->
@@ -309,6 +310,7 @@ let txt_of_inline_macro ~map_unicode_to_tex style ?flavour prefix name =
 (* procedural_txt_of_cic_term *)
 
 let procedural_txt_of_cic_term ~map_unicode_to_tex n ?depth context term =
+  let term, _info = PO.optimize_term context term in
   let annterm, ids_to_inner_sorts, ids_to_inner_types = 
      try Cic2acic.acic_term_of_cic_term context term
      with e -> 
@@ -327,6 +329,8 @@ let procedural_txt_of_cic_term ~map_unicode_to_tex n ?depth context term =
   String.concat "" (List.map aux script)
 ;;
 
+(****************************************************************************)
+
 let txt_of_macro ~map_unicode_to_tex metasenv context m =
    GrafiteAstPp.pp_macro
      ~term_pp:(txt_of_cic_term ~map_unicode_to_tex 80 metasenv context)