refactor: move ReplaceExpr to Init/Lean/Util

src/Init/Lean.lean

@@ -20,6 +20,6 @@ import Init.Lean.MetavarContext
 import Init.Lean.AuxRecursor
 import Init.Lean.Linter
 import Init.Lean.Meta
+import Init.Lean.Util
 import Init.Lean.Eval
 import Init.Lean.Structure
-import Init.Lean.ReplaceExpr

src/Init/Lean/Meta/Tactic/FVarSubst.lean

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Lean.Expr
-import Init.Lean.ReplaceExpr
+import Init.Lean.Util.ReplaceExpr
 
 namespace Lean
 namespace Meta

src/Init/Lean/Util.lean

@@ -0,0 +1,19 @@
+/-
+Copyright (c) 2020 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.Util.CollectFVars
+import Init.Lean.Util.CollectLevelParams
+import Init.Lean.Util.CollectMVars
+import Init.Lean.Util.FindMVar
+import Init.Lean.Util.MonadCache
+import Init.Lean.Util.PPExt
+import Init.Lean.Util.PPGoal
+import Init.Lean.Util.Path
+import Init.Lean.Util.Profile
+import Init.Lean.Util.RecDepth
+import Init.Lean.Util.Sorry
+import Init.Lean.Util.Trace
+import Init.Lean.Util.WHNF