refactor(library/tactic): move 'tracing' tactics to separate module
refactor(library/tactic): move 'exact' tactic to separate module
feat(library/tactic): add new approach for embedding non-elaborated expressions into tactics
refactor(library/tactic/rename_tactic): use new 'tactic.expr' to implement rename tactic
refactor(library/tactic/rename_tactic): use new 'tactic.expr' to implement 'intro/intros' tactic

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(frontends/lean): remove unnecessary files
refactor(frontends/lean): remove dead code
refactor(library/tactic): remove unnecessary hack

It is not needed anymore.
We had to use this hack when we had tactic_macro_definition_cell.
feat(library/tactic): change apply tactic semantics: goals are not reversed; and dependent arguments are not included

This commit also adds the tactic rapply that corresponds to the previous
semantics we have been using.
feat(library/tactic): elaborate 'exact' tactic argument at tactic execution time
fix(library/general_notation): mark \tr as left associative
feat(library/hott): add adjointification and closure properties for equivalences

Port features from the Coq Hott library
fix(library/hott) : convert to new path notations

Convert definitions and proofs to new notations for inverse and cocatenation. Adapt to now right associative of concatenation.
fix(library/hott) fix funext.lean to match equivalence notation
chore(library/hott): add Jakob to list of authors
refactor(library/tactic): add auxiliary module 'library/tactic/elaborate'
feat(library/tactic/elaborate): do not invoke unifier if no constraints were generated during elaboration
refactor(library/tactic): move 'unfold' tactic to separate module
fix(frontends/lean/elaborator): error localization for 'expr_to_tactic' failures
refactor(library/tactic/unfold_tactic): use new 'tactic.expr' to implement 'unfold' tactic

This change also enabled us to remove hacks used in the tests modified
by this commit.