X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2FapplyTransformation.ml;h=8e09d9db4809c241e7a969357667816fc719ce1e;hb=01b29f47d0d3e6c131fbdcc7a4180d428c8c97b9;hp=6cbad3b505d50cbcbce9ed8ab09075cec69ff0b3;hpb=bfcde2b08d72f1392ed61164c67d199360f0397f;p=helm.git

diff --git a/matita/matita/applyTransformation.ml b/matita/matita/applyTransformation.ml
index 6cbad3b50..8e09d9db4 100644
--- a/matita/matita/applyTransformation.ml
+++ b/matita/matita/applyTransformation.ml
@@ -35,36 +35,28 @@
 
 (* $Id$ *)
 
+class status =
+  object
+    inherit NTermCicContent.status
+    inherit TermContentPres.status
+  end
+
+
 let mpres_document pres_box =
   Xml.add_xml_declaration (CicNotationPres.print_box pres_box)
 
-let nmml_of_cic_sequent status metasenv subst sequent =
-  let content_sequent,ids_to_refs =
-   NTermCicContent.nmap_sequent status ~metasenv ~subst sequent in 
-  let pres_sequent = 
-   Sequent2pres.nsequent2pres ids_to_refs subst content_sequent in
-  let xmlpres = mpres_document pres_sequent in
-   Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres
-
 let ntxt_of_cic_sequent ~map_unicode_to_tex size status metasenv subst sequent =
   let content_sequent,ids_to_refs =
    NTermCicContent.nmap_sequent status ~metasenv ~subst sequent in 
   let pres_sequent = 
-   Sequent2pres.nsequent2pres ids_to_refs subst content_sequent in
+   Sequent2pres.nsequent2pres status ids_to_refs subst content_sequent in
   let pres_sequent = CicNotationPres.mpres_of_box pres_sequent in
    BoxPp.render_to_string ~map_unicode_to_tex
     (function x::_ -> x | _ -> assert false) size pres_sequent
 
-let nmml_of_cic_object status obj =
- let cobj,ids_to_nrefs = NTermCicContent.nmap_obj status 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 ntxt_of_cic_object ~map_unicode_to_tex size status obj =
  let cobj,ids_to_nrefs = NTermCicContent.nmap_obj status obj in 
- let pres_sequent = Content2pres.ncontent2pres ~ids_to_nrefs cobj in
+ let pres_sequent = Content2pres.ncontent2pres status ~ids_to_nrefs cobj in
  let pres_sequent = CicNotationPres.mpres_of_box pres_sequent in
   BoxPp.render_to_string ~map_unicode_to_tex
    (function x::_ -> x | _ -> assert false) size pres_sequent