From a68249393af9306d13cc35f80c541ed85aa2807b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 24 Feb 2020 13:18:07 -0800
Subject: [PATCH] chore: minimize dependencies

---
 src/Init/Lean/Elab/App.lean       | 1 +
 src/Init/Lean/Elab/Exception.lean | 2 +-
 src/Init/Lean/Elab/Level.lean     | 2 +-
 src/Init/Lean/Elab/Term.lean      | 5 ++++-
 src/Init/Lean/Meta.lean           | 4 ----
 src/Init/Lean/Meta/Basic.lean     | 3 +++
 6 files changed, 10 insertions(+), 7 deletions(-)

diff --git a/src/Init/Lean/Elab/App.lean b/src/Init/Lean/Elab/App.lean
index 4e3e99bd42..9e4ac2541c 100644
--- a/src/Init/Lean/Elab/App.lean
+++ b/src/Init/Lean/Elab/App.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Init.Lean.Util.FindMVar
 import Init.Lean.Elab.Term
 import Init.Lean.Elab.Binders
 
diff --git a/src/Init/Lean/Elab/Exception.lean b/src/Init/Lean/Elab/Exception.lean
index 37654a4dd3..30f35017ca 100644
--- a/src/Init/Lean/Elab/Exception.lean
+++ b/src/Init/Lean/Elab/Exception.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Lean.Meta
+import Init.Lean.Meta.Message
 
 namespace Lean
 namespace Elab
diff --git a/src/Init/Lean/Elab/Level.lean b/src/Init/Lean/Elab/Level.lean
index 46555dece5..611da2e1c8 100644
--- a/src/Init/Lean/Elab/Level.lean
+++ b/src/Init/Lean/Elab/Level.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Lean.Meta
+import Init.Lean.Meta.LevelDefEq
 import Init.Lean.Elab.Exception
 import Init.Lean.Elab.Log
 
diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean
index 42920558b8..23f922918a 100644
--- a/src/Init/Lean/Elab/Term.lean
+++ b/src/Init/Lean/Elab/Term.lean
@@ -6,7 +6,10 @@ Authors: Leonardo de Moura
 prelude
 import Init.Lean.Util.Sorry
 import Init.Lean.Structure
-import Init.Lean.Meta
+import Init.Lean.Meta.ExprDefEq
+import Init.Lean.Meta.AppBuilder
+import Init.Lean.Meta.SynthInstance
+import Init.Lean.Meta.Tactic.Util
 import Init.Lean.Hygiene
 import Init.Lean.Util.RecDepth
 import Init.Lean.Elab.Log
diff --git a/src/Init/Lean/Meta.lean b/src/Init/Lean/Meta.lean
index 81d49dc427..75e15b4236 100644
--- a/src/Init/Lean/Meta.lean
+++ b/src/Init/Lean/Meta.lean
@@ -20,7 +20,3 @@ import Init.Lean.Meta.Tactic
 import Init.Lean.Meta.Message
 import Init.Lean.Meta.KAbstract
 import Init.Lean.Meta.RecursorInfo
-
-namespace Lean
-export Meta (MetaM)
-end Lean
diff --git a/src/Init/Lean/Meta/Basic.lean b/src/Init/Lean/Meta/Basic.lean
index 53820e415b..4b5664efcd 100644
--- a/src/Init/Lean/Meta/Basic.lean
+++ b/src/Init/Lean/Meta/Basic.lean
@@ -819,6 +819,9 @@ match x { maxRecDepth := maxRecDepth, currRecDepth := 0 } { env := env } with
 | EStateM.Result.error ex _ => Except.error ex
 
 end Meta
+
+export Meta (MetaM)
+
 end Lean
 
 open Lean