X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2FapplyTransformation.ml;h=4015293a435907f7a24f29f20b5824fb14e05cc1;hb=f3c6deea5fa1ed58847d7fcdf597193e2c5c7ddb;hp=da4bccba0adff65b2f54d79d1f9e19fc37f09a77;hpb=11b2157bacf59cfc561c2ef6f92ee41ee2c1a006;p=helm.git

diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml
index da4bccba0..4015293a4 100644
--- a/helm/software/matita/applyTransformation.ml
+++ b/helm/software/matita/applyTransformation.ml
@@ -90,8 +90,10 @@ let mml_of_cic_object obj =
   ids_to_inner_sorts,ids_to_inner_types)))
 
 let nmml_of_cic_object obj =
- prerr_endline (NCicPp.ppobj obj);
- assert false
+ let cobj,ids_to_nrefs = NTermCicContent.nmap_obj obj in 
+ let pres_sequent = Content2pres.ncontent2pres ~ids_to_nrefs cobj in
+ let xmlpres = mpres_document pres_sequent in
+  Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres
 ;;
 
 let txt_of_cic_sequent ~map_unicode_to_tex size metasenv sequent =
@@ -232,9 +234,13 @@ let txt_of_cic_object
      let aux = function
 	| G.Executable (_, G.Command (_, G.Obj (_, N.Inductive _))) as stm
 	      -> 	   
+	   let hc = !Acic2content.hide_coercions in
+	   if List.mem G.IPCoercions params then 
+	      Acic2content.hide_coercions := false;
 	   enable_notations false;
 	   let str = stm_pp stm in 
 	   enable_notations true;
+	   Acic2content.hide_coercions := hc;
 	   str
 (* FG: we disable notation for Inductive to avoid recursive notation *) 
 	| G.Executable (_, G.Tactic _) as stm -> 
@@ -244,7 +250,13 @@ let txt_of_cic_object
 	   Acic2content.hide_coercions := hc;
            str
 (* FG: we show coercion because the reconstruction is not aware of them *)
-	| stm -> stm_pp stm
+	| stm -> 
+	   let hc = !Acic2content.hide_coercions in
+	   if List.mem G.IPCoercions params then 
+	      Acic2content.hide_coercions := false;
+	   let str = stm_pp stm in
+	   Acic2content.hide_coercions := hc;
+           str
      in
      let script = 
         Acic2Procedural.procedural_of_acic_object