- libraryObjects: new default "natural numbers" with the uri of nat.

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

diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml
index 0364803c73d82c8552aa4e01b9e3b7d6b1c1f165..a397de41e8fa3b8b82b930968a1ef1251d45baec 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralOptimizer.ml
+++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml
@@ -99,7 +99,9 @@ let rec opt_letin g st es c name v w t =
          | v when H.is_proof c v && H.is_atomic v          ->
            let x = S.subst v t in
            opt_proof g (info st "Optimizer: remove 5") true c x 
-        | v                                               ->
+(*      | v when t = C.Rel 1                              ->
+           g (info st "Optimizer: remove 6") v 
+*)      | v                                               ->
            g st (C.LetIn (name, v, w, t))
       in
       if es then opt_term g st es c v else g st v