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