X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FapplyTransformation.ml;h=670fd2e0c5d8fb7dd4e87cba43baa41aa4f98253;hb=700b170aa9b0377d33f1edd44de8d89129477fb8;hp=ac044cefed05b15bc5810636555893e02101b5a1;hpb=9e010764b6de0d8a268a6ecb83e8e90246bee129;p=helm.git

diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml
index ac044cefe..670fd2e0c 100644
--- a/helm/software/matita/applyTransformation.ml
+++ b/helm/software/matita/applyTransformation.ml
@@ -204,7 +204,15 @@ let txt_of_cic_object
             (CicNotationPres.mpres_of_box bobj)
         )
      | G.Procedural depth ->
+(*
+        PO.critical := false;
+	Acic2Procedural.tex_formatter := Some Format.std_formatter;	
+	let _ = ProceduralTeX.tex_of_obj Format.std_formatter obj in
+*)	
 	let obj, info = PO.optimize_obj obj in
+(*	
+	let _ = ProceduralTeX.tex_of_obj Format.std_formatter 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
@@ -244,6 +252,9 @@ let discharge_uri style uri =
 let discharge_name s = s ^ "_discharged"
 
 let txt_of_inline_uri ~map_unicode_to_tex style ?flavour prefix suri =
+(*   
+   Ds.debug := true;
+*)
    let print_exc = function
       | ProofEngineHelpers.Bad_pattern s as e ->
            Printexc.to_string e ^ " " ^ Lazy.force s
@@ -280,7 +291,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 ->