Bug fixed: variable capture in previous commit prevented all aliases insertion.

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

diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml
index e741ed70c4ba8c79f1f88488057bd51522487b27..c504996e0d225e18ebe89e83e0188e680a0994eb 100644 (file)
--- a/helm/software/matita/applyTransformation.ml
+++ b/helm/software/matita/applyTransformation.ml
@@ -64,6 +64,13 @@ let mml_of_cic_sequent metasenv sequent =
    (asequent,
     (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 = NTermCicContent.nmap_sequent ~subst sequent in 
+  let pres_sequent = 
+   Sequent2pres.nsequent2pres subst content_sequent in
+  let xmlpres = mpres_document pres_sequent in
+   Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres
+
 let mml_of_cic_object obj =
   let (annobj, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
     ids_to_inner_types, ids_to_conjectures, ids_to_hypotheses)
@@ -204,7 +211,15 @@ let txt_of_cic_object
             (CicNotationPres.mpres_of_box bobj)
         )
      | G.Procedural depth ->
+(*
+        PO.critical := false;
+       Acic2Procedural.tex_formatter := Some Format.std_formatter;     
+       let _ = ProceduralTeX.tex_of_obj Format.std_formatter obj in
+*)     
        let obj, info = PO.optimize_obj obj in
+(*     
+       let _ = ProceduralTeX.tex_of_obj Format.std_formatter obj in
+*)     
         let aobj, ids_to_inner_sorts, ids_to_inner_types = get_aobj obj in
         let term_pp = term2pres ~map_unicode_to_tex (n - 8) ids_to_inner_sorts in
         let lazy_term_pp = term_pp in
@@ -244,6 +259,9 @@ let discharge_uri style uri =
 let discharge_name s = s ^ "_discharged"
 
 let txt_of_inline_uri ~map_unicode_to_tex style ?flavour prefix suri =
+(*   
+   Ds.debug := true;
+*)
    let print_exc = function
       | ProofEngineHelpers.Bad_pattern s as e ->
            Printexc.to_string e ^ " " ^ Lazy.force s