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 208864c801f1a2fdeafa99506ade65b46f901f51..9a1b0e3ca981c08197abfc6f4affd0b3121aeb5f 100644 (file)
--- 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