From 4cafd19f7227177020b026482bedb70bb487178b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 3 May 2019 09:11:12 -0700 Subject: [PATCH] chore(library/init/lean/compiler): missing `prelude` --- library/init/lean/compiler/elimdead.lean | 1 + library/init/lean/compiler/pushproj.lean | 1 + library/init/lean/compiler/simpcase.lean | 1 + 3 files changed, 3 insertions(+) diff --git a/library/init/lean/compiler/elimdead.lean b/library/init/lean/compiler/elimdead.lean index 934c415fdf..ae86da4be0 100644 --- a/library/init/lean/compiler/elimdead.lean +++ b/library/init/lean/compiler/elimdead.lean @@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +prelude import init.lean.compiler.ir namespace Lean diff --git a/library/init/lean/compiler/pushproj.lean b/library/init/lean/compiler/pushproj.lean index ae54c4f4d9..3b35c5ca62 100644 --- a/library/init/lean/compiler/pushproj.lean +++ b/library/init/lean/compiler/pushproj.lean @@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +prelude import init.lean.compiler.ir namespace Lean diff --git a/library/init/lean/compiler/simpcase.lean b/library/init/lean/compiler/simpcase.lean index 5f4e44950b..91750ce260 100644 --- a/library/init/lean/compiler/simpcase.lean +++ b/library/init/lean/compiler/simpcase.lean @@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +prelude import init.lean.compiler.ir namespace Lean