This commit restores the ids_to_father_ids table.

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

diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml
index da4bccba0adff65b2f54d79d1f9e19fc37f09a77..e23400fb2c910a46436532101fdb32073555b339 100644 (file)
--- a/helm/software/matita/applyTransformation.ml
+++ b/helm/software/matita/applyTransformation.ml
@@ -66,12 +66,12 @@ let mml_of_cic_sequent metasenv sequent =
     (ids_to_terms,ids_to_father_ids,ids_to_hypotheses,ids_to_inner_sorts)))
 
 let nmml_of_cic_sequent metasenv subst sequent =
-  let content_sequent,ids_to_refs =
+  let content_sequent,ids_to_refs,ids_to_father_ids =
    NTermCicContent.nmap_sequent ~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
+   Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres,ids_to_father_ids
 
 let mml_of_cic_object obj =
   let (annobj, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
@@ -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,ids_to_father_ids = 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,ids_to_father_ids
 ;;
 
 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