diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean
index 7b9ee1f1fe..a839e2de70 100644
--- a/library/init/meta/simp_tactic.lean
+++ b/library/init/meta/simp_tactic.lean
@@ -358,13 +358,6 @@ step $
 do s ← collect_ctx_simps >>= s.append,
    simp_intro_aux cfg tt s tt ns
 
-meta def replace_hyp (h : expr) (h_new_type : expr) (pr : expr) : tactic expr :=
-do h_type ← infer_type h,
-   new_h ← assert h.local_pp_name h_new_type,
-   mk_eq_mp pr h >>= exact,
-   try $ clear h,
-   return new_h
-
 meta def simp_at (h : expr) (extra_lemmas : list expr := []) (cfg : simp_config := {}) : tactic expr :=
 do when (expr.is_local_constant h = ff) (fail "tactic simp_at failed, the given expression is not a hypothesis"),
    htype ← infer_type h,
diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index 2d3d6927ff..630ed8ea5e 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -1077,6 +1077,19 @@ do h ← get_local curr,
    intro new,
    intron (n - 1)
 
+/--
+"Replace" hypothesis `h : type` with `h : new_type` where `eq_pr` is a proof
+that (type = new_type). The tactic actually creates a new hypothesis
+with the same user facing name, and (tries to) clear `h`.
+The `clear` step fails if `h` has forward dependencies. In this case, the old `h`
+will remain in the local context. The tactic returns the new hypothesis. -/
+meta def replace_hyp (h : expr) (new_type : expr) (eq_pr : expr) : tactic expr :=
+do h_type ← infer_type h,
+   new_h ← assert h.local_pp_name new_type,
+   mk_eq_mp eq_pr h >>= exact,
+   try $ clear h,
+   return new_h
+
 end tactic
 
 notation [parsing_only] `command`:max := tactic unit