- Procedural convertible rewrites in the conclusion are now detected and replaced...

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

diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml
index 91fe7bcd0ca2e6cbd570b5177f9c980e0dda32da..4015293a435907f7a24f29f20b5824fb14e05cc1 100644 (file)
--- a/helm/software/matita/applyTransformation.ml
+++ b/helm/software/matita/applyTransformation.ml
@@ -234,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 -> 
@@ -246,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