diff --git a/doc/changes.md b/doc/changes.md
index 3fddec2a23..8d2b779e34 100644
--- a/doc/changes.md
+++ b/doc/changes.md
@@ -44,6 +44,8 @@ master branch (aka work in progress branch)
 
 *Changes*
 
+- `cases h` now also tries to clear `h` when performing dependent elimination.
+
 - `repeat { t }` behavior changed. Now, it applies `t` to each goal. If the application succeeds,
   the tactic is applied recursively to all the generated subgoals until it eventually fails.
   The recursion stops in a subgoal when the tactic has failed to make progress.
diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index fd37e85658..1c0e9a28ef 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -1193,12 +1193,14 @@ do e ← to_expr p, guard (alpha_eqv t e)
 
 /--
 `guard_target t` fails if the target of the main goal is not `t`.
+We use this tactic for writing tests.
 -/
 meta def guard_target (p : parse texpr) : tactic unit :=
 do t ← target, guard_expr_eq t p
 
 /--
 `guard_hyp h := t` fails if the hypothesis `h` does not have type `t`.
+We use this tactic for writing tests.
 -/
 meta def guard_hyp (n : parse ident) (p : parse $ tk ":=" *> texpr) : tactic unit :=
 do h ← get_local n >>= infer_type, guard_expr_eq h p