From 4b896bc71c3d21edf48fe61d53e4f3fa8355818c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 24 May 2019 19:20:20 -0700 Subject: [PATCH] fix(library/init/lean/compiler/ir/rc): use updated ctx at `addDecForAlt` Compiler was introducing unnecessary `dec` operations --- library/init/lean/compiler/ir/rc.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/library/init/lean/compiler/ir/rc.lean b/library/init/lean/compiler/ir/rc.lean index e9d756b4a9..677f6f6ec0 100644 --- a/library/init/lean/compiler/ir/rc.lean +++ b/library/init/lean/compiler/ir/rc.lean @@ -247,7 +247,8 @@ partial def visitFnBody : FnBody → Context → (FnBody × LiveVarSet) let caseLiveVars := collectLiveVars b ctx.jpLiveVarMap in let alts := alts.hmap $ λ alt, match alt with | Alt.ctor c b := - let (b, altLiveVars) := visitFnBody b (updateRefUsingCtorInfo ctx x c) in + let ctx := updateRefUsingCtorInfo ctx x c in + let (b, altLiveVars) := visitFnBody b ctx in let b := addDecForAlt ctx caseLiveVars altLiveVars b in Alt.ctor c b | Alt.default b :=