From 3dbe2076b94fa704d07beb79d96890ab224477ca Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 17 Sep 2020 13:59:22 -0700
Subject: [PATCH] refactor: `Target`&`LocalDecl` => `Replace`

---
 src/Lean/Meta/Tactic.lean                     |  3 +--
 src/Lean/Meta/Tactic/LocalDecl.lean           | 24 -------------------
 .../Meta/Tactic/{Target.lean => Replace.lean} | 10 ++++++++
 3 files changed, 11 insertions(+), 26 deletions(-)
 delete mode 100644 src/Lean/Meta/Tactic/LocalDecl.lean
 rename src/Lean/Meta/Tactic/{Target.lean => Replace.lean} (85%)

diff --git a/src/Lean/Meta/Tactic.lean b/src/Lean/Meta/Tactic.lean
index 07715bfa4e..c06dab4c1b 100644
--- a/src/Lean/Meta/Tactic.lean
+++ b/src/Lean/Meta/Tactic.lean
@@ -9,9 +9,8 @@ import Lean.Meta.Tactic.Apply
 import Lean.Meta.Tactic.Revert
 import Lean.Meta.Tactic.Clear
 import Lean.Meta.Tactic.Assert
-import Lean.Meta.Tactic.Target
 import Lean.Meta.Tactic.Rewrite
 import Lean.Meta.Tactic.Generalize
-import Lean.Meta.Tactic.LocalDecl
+import Lean.Meta.Tactic.Replace
 import Lean.Meta.Tactic.Induction
 import Lean.Meta.Tactic.Cases
diff --git a/src/Lean/Meta/Tactic/LocalDecl.lean b/src/Lean/Meta/Tactic/LocalDecl.lean
deleted file mode 100644
index c297fa467c..0000000000
--- a/src/Lean/Meta/Tactic/LocalDecl.lean
+++ /dev/null
@@ -1,24 +0,0 @@
-/-
-Copyright (c) 2020 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-import Lean.Meta.AppBuilder
-import Lean.Meta.Tactic.Util
-import Lean.Meta.Tactic.Assert
-import Lean.Meta.Tactic.Intro
-import Lean.Meta.Tactic.Clear
-
-namespace Lean
-namespace Meta
-
-def replaceLocalDecl (mvarId : MVarId) (fvarId : FVarId) (newType : Expr) (eqProof : Expr) : MetaM (FVarId × MVarId) := do
-withMVarContext mvarId $ do
-  localDecl ← getLocalDecl fvarId;
-  newTypePr ← mkEqMP eqProof (mkFVar fvarId);
-  mvarId ← assert mvarId localDecl.userName newType newTypePr;
-  (fvarIdNew, mvarId) ← intro1 mvarId;
-  (do mvarId ← clear mvarId fvarId; pure (fvarIdNew, mvarId)) <|> pure (fvarIdNew, mvarId)
-
-end Meta
-end Lean
diff --git a/src/Lean/Meta/Tactic/Target.lean b/src/Lean/Meta/Tactic/Replace.lean
similarity index 85%
rename from src/Lean/Meta/Tactic/Target.lean
rename to src/Lean/Meta/Tactic/Replace.lean
index c3db6539cf..62ea82ac12 100644
--- a/src/Lean/Meta/Tactic/Target.lean
+++ b/src/Lean/Meta/Tactic/Replace.lean
@@ -7,6 +7,8 @@ import Lean.Meta.AppBuilder
 import Lean.Meta.Tactic.Util
 import Lean.Meta.Tactic.Revert
 import Lean.Meta.Tactic.Intro
+import Lean.Meta.Tactic.Clear
+import Lean.Meta.Tactic.Assert
 
 namespace Lean
 namespace Meta
@@ -46,6 +48,14 @@ withMVarContext mvarId do
     assignExprMVar mvarId newMVar;
     pure newMVar.mvarId!
 
+def replaceLocalDecl (mvarId : MVarId) (fvarId : FVarId) (newType : Expr) (eqProof : Expr) : MetaM (FVarId × MVarId) := do
+withMVarContext mvarId $ do
+  localDecl ← getLocalDecl fvarId;
+  newTypePr ← mkEqMP eqProof (mkFVar fvarId);
+  mvarId ← assert mvarId localDecl.userName newType newTypePr;
+  (fvarIdNew, mvarId) ← intro1 mvarId;
+  (do mvarId ← clear mvarId fvarId; pure (fvarIdNew, mvarId)) <|> pure (fvarIdNew, mvarId)
+
 def change (mvarId : MVarId) (targetNew : Expr) : MetaM MVarId :=
 withMVarContext mvarId do
   target ← getMVarType mvarId;