X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralOptimizer.ml;h=1953ae7f1b6a5c385fcdbb6aad65b76740a15a28;hb=3e25c8d9f6e7802a2fc28697795b9128af731494;hp=19d96a91aa7ef042f7113656a43cb8a4ce99f4fa;hpb=2921483dad22e14c2e697cbe5597a0b32af04090;p=helm.git

diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml
index 19d96a91a..1953ae7f1 100644
--- a/helm/software/components/acic_procedural/proceduralOptimizer.ml
+++ b/helm/software/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
@@ -260,6 +263,7 @@ and opt2_term g c t =
 
 let optimize_obj = function
    | C.Constant (name, Some bo, ty, pars, attrs) ->
+      let bo, ty = H.cic_bc [] bo, H.cic_bc [] ty in 
       let g bo = 
          Printf.eprintf "Optimized : %s\nPost Nodes: %u\n" 
 	    (Pp.ppterm bo) (I.count_nodes 0 bo);