applyTransformation: added debugging information

[helm.git] / components / acic_procedural / proceduralOptimizer.ml

diff --git a/components/acic_procedural/proceduralOptimizer.ml b/components/acic_procedural/proceduralOptimizer.ml
index 19d96a91aa7ef042f7113656a43cb8a4ce99f4fa..9d04c2f91f89d0c78667c50f1c5076c56e333065 100644 (file)
--- a/components/acic_procedural/proceduralOptimizer.ml
+++ b/components/acic_procedural/proceduralOptimizer.ml
@@ -72,7 +72,10 @@ let rec opt1_letin g es c name v t =
          | C.LetIn (nname, vv, tt) when H.is_proof c v ->
            let x = C.LetIn (nname, vv, C.LetIn (name, tt, S.lift_from 2 1 t)) in
            HLog.warn "Optimizer: swap 1"; opt1_proof g true c x 
-         | v                               -> 
+         | v when H.is_proof c v && H.is_atomic v     ->
+           let x = S.subst v t in
+           HLog.warn "Optimizer: remove 5"; opt1_proof g true c x 
+        | v                                           -> 
            g (C.LetIn (name, v, t))
       in
       if es then opt1_term g es c v else g v