From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 6 Dec 2002 13:31:28 +0000 (+0000)
Subject: Bug fixed: when iota-expanding fixpoints the context was sometimes augmented
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9f694d4bf47c7772dda4827f1b46f42cb435ec36;p=helm.git

Bug fixed: when iota-expanding fixpoints the context was sometimes augmented
with the new types, even if the expansion already de-lifted the function body.
---

diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml
index 208864c80..9a1b0e3ca 100644
--- a/helm/gTopLevel/proofEngineReduction.ml
+++ b/helm/gTopLevel/proofEngineReduction.ml
@@ -344,7 +344,7 @@ let reduce context =
                  fl
                  body
               in
-               reduceaux (tys@context) [] body'
+               reduceaux context [] body'
          | C.Appl (C.CoFix (i,fl) :: tl) ->
             let tys =
              List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
@@ -358,7 +358,7 @@ let reduce context =
                  body
               in
                let tl' = List.map (reduceaux context []) tl in
-                reduceaux (tys@context) tl' body'
+                reduceaux context tl' body'
          | t -> t
        in
         (match decofix (reduceaux context [] term) with
@@ -575,7 +575,7 @@ let simpl context =
                              in
                               (* Possible optimization: substituting whd *)
                               (* recparam in l                           *)
-                              reduceaux (tys@context) l body',
+                              reduceaux context l body',
                                List.rev rev_constant_args
                           | _ -> raise AlreadySimplified
                         )
@@ -642,7 +642,7 @@ let simpl context =
                  fl
                  body
               in
-               reduceaux (tys@context) [] body'
+               reduceaux context [] body'
          | C.Appl (C.CoFix (i,fl) :: tl) ->
             let tys =
              List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl            in
@@ -655,7 +655,7 @@ let simpl context =
                  body
               in
                let tl' = List.map (reduceaux context []) tl in
-                reduceaux (tys@context) tl body'
+                reduceaux context tl body'
          | t -> t
        in
         (match decofix (reduceaux context [] term) with