diff --git a/library/Init/Lean/Compiler/IR/Borrow.lean b/library/Init/Lean/Compiler/IR/Borrow.lean index 957012928f..0797b58d94 100644 --- a/library/Init/Lean/Compiler/IR/Borrow.lean +++ b/library/Init/Lean/Compiler/IR/Borrow.lean @@ -308,7 +308,6 @@ end Borrow def inferBorrow (decls : Array Decl) : CompilerM (Array Decl) := do env ← getEnv; - let decls := decls.map Decl.normalizeIds; let paramMap := Borrow.infer env decls; pure (Borrow.applyParamMap decls paramMap) diff --git a/library/Init/Lean/Compiler/IR/EmitC.lean b/library/Init/Lean/Compiler/IR/EmitC.lean index 47459f83fb..d91c5f95d9 100644 --- a/library/Init/Lean/Compiler/IR/EmitC.lean +++ b/library/Init/Lean/Compiler/IR/EmitC.lean @@ -624,7 +624,7 @@ do env ← getEnv; | _ => pure () def emitDecl (d : Decl) : M Unit := -let d := d.normalizeIds; +let d := d.normalizeIds; -- ensure we don't have gaps in the variable indices catch (emitDeclAux d) (fun err => throw (err ++ "\ncompiling:\n" ++ toString d)) diff --git a/library/Init/Lean/Compiler/IR/ExpandResetReuse.lean b/library/Init/Lean/Compiler/IR/ExpandResetReuse.lean index 557cc71d9d..c456c9270e 100644 --- a/library/Init/Lean/Compiler/IR/ExpandResetReuse.lean +++ b/library/Init/Lean/Compiler/IR/ExpandResetReuse.lean @@ -275,7 +275,6 @@ partial def searchAndExpand : FnBody → Array FnBody → M FnBody else searchAndExpand b.body (push bs b) def main (d : Decl) : Decl := -let d := d.normalizeIds; match d with | (Decl.fdecl f xs t b) => let m := mkProjMap d;