1) the home button of CicBrowser now works also for NG

[helm.git] / helm / software / matita / applyTransformation.ml

diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml
index da4bccba0adff65b2f54d79d1f9e19fc37f09a77..91fe7bcd0ca2e6cbd570b5177f9c980e0dda32da 100644 (file)
--- 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 =