From: Claudio Sacerdoti Coen 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