]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/applyTransformation.ml
Procedural: refactoring
[helm.git] / matita / applyTransformation.ml
index cff93ace3458413cf2e4089c36a9df3cde4d5709..de87d55489c1ce31ef855550301a976c08c1c68f 100644 (file)
@@ -179,7 +179,7 @@ let txt_of_cic_object ?map_unicode_to_tex n style prefix obj =
             (CicNotationPres.mpres_of_box bobj)
        )
      | G.Procedural depth ->
-        let obj = ProceduralPreprocess.pp_obj obj in
+        let obj = ProceduralOptimizer.optimize_obj obj in
        let aobj, ids_to_inner_sorts, ids_to_inner_types = get_aobj obj in
         let term_pp = term2pres (n - 8) ids_to_inner_sorts in
         let lazy_term_pp = term_pp in