From 7e963807112aabe5ec03002fa27181a36d20e607 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 25 Feb 2020 10:59:56 -0800 Subject: [PATCH] chore: remove unnecessary import --- src/Init/Lean/Compiler/IR/UnboxResult.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Init/Lean/Compiler/IR/UnboxResult.lean b/src/Init/Lean/Compiler/IR/UnboxResult.lean index f29cad6559..818008c6f8 100644 --- a/src/Init/Lean/Compiler/IR/UnboxResult.lean +++ b/src/Init/Lean/Compiler/IR/UnboxResult.lean @@ -6,7 +6,6 @@ Authors: Leonardo de Moura prelude import Init.Lean.Data.Format import Init.Lean.Compiler.IR.Basic -import Init.Lean.Compiler.IR.CtorLayout namespace Lean namespace IR