X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralOptimizer.ml;h=a05bbd26d8df836d422b6fee82dd838b44840281;hb=5b45f78ed4293ebbe8cc73ad925bca11a300d021;hp=f1840cf7c95c75cf37877712fdfa70fdb66caa34;hpb=a57ca0d68754b946b33976acf2e72f45ff11c8d7;p=helm.git

diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml
index f1840cf7c..a05bbd26d 100644
--- a/helm/software/components/acic_procedural/proceduralOptimizer.ml
+++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml
@@ -209,8 +209,14 @@ and opt_mutcase_critical g st es c uri tyno outty arg cases =
    opt_proof g (info st "Optimizer: remove 3") es c x
 
 and opt_mutcase_plain g st es c uri tyno outty arg cases =
-   let g st v ts = g st (C.MutCase (uri, tyno, outty, v, ts)) in
-   g st arg cases
+   let g st v =
+      let g (st, ts) = g st (C.MutCase (uri, tyno, outty, v, ts)) in
+      let map h v (st, vs) =
+         let h st vv = h (st, vv :: vs) in opt_proof h st es c v
+      in
+      if es then H.list_fold_right_cps g map cases (st, []) else g (st, cases)
+   in
+   if es then opt_proof g st es c arg else g st arg
 
 and opt_mutcase g =
    if !critical then opt_mutcase_critical g else opt_mutcase_plain g