PrimitiveTactics: intros _ now aveilable

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

diff --git a/components/acic_procedural/proceduralOptimizer.ml b/components/acic_procedural/proceduralOptimizer.ml
index 9d95d100ba83c375d1ba9f35d17d8ca73268b90c..ab15d70872aeccf94f99493eabc8511a577dbfb1 100644 (file)
--- a/components/acic_procedural/proceduralOptimizer.ml
+++ b/components/acic_procedural/proceduralOptimizer.ml
@@ -82,10 +82,7 @@ let rec opt1_letin g es c name v t =
 and opt1_lambda g es c name w t =
    let name = H.mk_fresh_name c name in
    let entry = Some (name, C.Decl w) in
-   let g t = 
-      let name = if DTI.does_not_occur 1 t then C.Anonymous else name in
-      g (C.Lambda (name, w, t))
-   in
+   let g t = g (C.Lambda (name, w, t)) in
    if es then opt1_proof g es (entry :: c) t else g t
 
 and opt1_appl g es c t vs =