chore(library/init/meta/interactive): add comment to avoid confusion

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.

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