From 36b723193c021125b05afe0106fc3ed8d674bea7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 17 Feb 2020 18:41:13 -0800
Subject: [PATCH] refactor: move `ReplaceExpr` to `Init/Lean/Util`

---
 src/Init/Lean.lean                        |  2 +-
 src/Init/Lean/Meta/Tactic/FVarSubst.lean  |  2 +-
 src/Init/Lean/Util.lean                   | 19 +++++++++++++++++++
 src/Init/Lean/{ => Util}/ReplaceExpr.lean |  0
 4 files changed, 21 insertions(+), 2 deletions(-)
 create mode 100644 src/Init/Lean/Util.lean
 rename src/Init/Lean/{ => Util}/ReplaceExpr.lean (100%)

diff --git a/src/Init/Lean.lean b/src/Init/Lean.lean
index cc803ea7a6..d6a06d2312 100644
--- a/src/Init/Lean.lean
+++ b/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
diff --git a/src/Init/Lean/Meta/Tactic/FVarSubst.lean b/src/Init/Lean/Meta/Tactic/FVarSubst.lean
index a5689b9ffc..b7d636023d 100644
--- a/src/Init/Lean/Meta/Tactic/FVarSubst.lean
+++ b/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
diff --git a/src/Init/Lean/Util.lean b/src/Init/Lean/Util.lean
new file mode 100644
index 0000000000..49d8d7f2cb
--- /dev/null
+++ b/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
diff --git a/src/Init/Lean/ReplaceExpr.lean b/src/Init/Lean/Util/ReplaceExpr.lean
similarity index 100%
rename from src/Init/Lean/ReplaceExpr.lean
rename to src/Init/Lean/Util/ReplaceExpr.lean