primed tactics from mathlib

Here's a list of "primed" tactics in mathlib which fix bugs or add features to tactics in the core library. I'm not sure which of these should replace their counterparts, if someone else can review this that'd be great. (Feel free to edit this list directly!)

I can try to tackle the ones from tactic.core and tactic.interactive which don't require modifying C++.

Primed tactics in mathlib's tactic.core:

• of_tactic' / has_coe' replaces of_tactic and has_coe in init.lean.parser. of_tactic is implemented in C++ here. of_tactic' was removed in the 3.7.1c update since it was no longer necessary after the fix in #147.

• eval_expr' replaces eval_expr in init.meta.tactic; C++ implementation here.

• has_attribute' returns a bool whereas has_attribute in init.meta.tactic returns a nat; C++ implementation here.

• simp_bottom_up' "a variant" of simplify_bottom_up.

• triv': "Unlike triv, it only unfolds reducible definitions, so it sometimes fails faster."

- [ ] iterate', compare iterate in init.meta.tactic.

- [ ] target' is a wrapper around target (C++ implementation here) that instantiates mvars and calls whnf.

• resolve_name' wraps resolve_name (C++ implementation here) so that it succeeds on a list of empty goals.

Primed tactics in mathlib's tactic.interactive:

• congr' behaves like congr but takes an optional argument specifying the depth of recursive applications.

• guard_hyp' fixes guard_hyp by instantiating meta variables.

- [ ] guard_expr_eq' uses is_def_eq, whereas guard_expr_eq uses alpha_eqv.

- [ ] guard_target' uses guard_expr_eq', whereas guard_target uses guard_expr_eq.

• change' "mimics the behavior of change, except in the case of change x with y at l. In this case, it will correctly replace occurences of x with y at all possible hypotheses in l. As long as x and y are defeq, it should never fail."

Other primed tactics in mathlib:

• rename' adds several features to rename. Ported in #205.

• apply' / symmetry' / reflexivity' / transitivity' / ... fixes the "apply bug" in apply and related tactics (also in init.meta.interactive). See also apply_fun.

• clear' works like clear (C++ implementation here) except that the hypotheses can be cleared in any order. See also clear_dependent in the same file.

Any others?

Start by comparing the primed implementations in mathlib's src/tactic/core.lean, src/tactic/interactive.lean, src/tactic/apply.lean, and src/tactic/clear.lean with their counterparts under Lean's library/init/meta files and the linked C++ implementations. Done requires an agreed, reviewed scope for which tactics should replace their core counterparts, including any required changes to the core implementation.