X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FapplyTransformation.ml;h=236e59def34becbb6654780f2d3f7d42779fbc18;hb=f9f775a550264a8dc9ce7ea9a48b79892a122c3c;hp=8e09d9db4809c241e7a969357667816fc719ce1e;hpb=10d33a8c1be31d0c7aeccee8968fd5218ca2510a;p=helm.git diff --git a/matita/matita/applyTransformation.ml b/matita/matita/applyTransformation.ml index 8e09d9db4..236e59def 100644 --- a/matita/matita/applyTransformation.ml +++ b/matita/matita/applyTransformation.ml @@ -36,18 +36,17 @@ (* $Id$ *) class status = - object - inherit NTermCicContent.status - inherit TermContentPres.status - end - + object + inherit Interpretations.status + inherit TermContentPres.status + end let mpres_document pres_box = Xml.add_xml_declaration (CicNotationPres.print_box pres_box) 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 + Interpretations.nmap_sequent status ~metasenv ~subst sequent in let pres_sequent = Sequent2pres.nsequent2pres status ids_to_refs subst content_sequent in let pres_sequent = CicNotationPres.mpres_of_box pres_sequent in @@ -55,7 +54,7 @@ let ntxt_of_cic_sequent ~map_unicode_to_tex size status metasenv subst sequent = (function x::_ -> x | _ -> assert false) size pres_sequent let ntxt_of_cic_object ~map_unicode_to_tex size status obj = - let cobj,ids_to_nrefs = NTermCicContent.nmap_obj status obj in + let cobj,ids_to_nrefs = Interpretations.nmap_obj status obj 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