feat(frontends/lean): add option 'pp.purify_locals'
fix(library/tactic/inversion_tactic): bug in name generation
feat(library/tactic): 'exact' tactic report unsolved placeholders in nested expression

Actually, the elaborator is the one reporting the unassigned
placeholders. The 'exact' tactic just makes the request.
To implement this feature we had to extend the elaboration interface
expected by the tactic framework.
fix(linja): incorrect output when maximum number of errors/warnings was reached, fixes #352
feat(frontends/lean): add option 'elaborator.flycheck_goals'
feat(library/tools/tactic): add 'cases' alias for 'inversion' tactic
feat(library/tactic): refine 'get_unused_name'
fix(frontends/lean/elaborator): do not display flycheck related messages when --flycheck is not on
feat(library/tactic/inversion_tactic): basic 'inversion' tactic
fix(library/tactic/inversion_tactic): bug in injectivity transition
feat(library/tactic/inversion_tactic): add 'case ... with ...' variant that allows user to specify names for new hypotheses
fix(emacs): syntax highlight for 'cases ... with ...'
refactor(library/data/fin): simplify 'fin' module using new inversion tactic
chore(library/hott) change equiv.lean to use structures and more typeclass inference
chore(library/hott) change naming to leo's naming proposal
chore(library/hott) change naming in equiv_precomp
chore(library/hott) change is_pointed to structure
feat(library/data/sum): use + notation for sum
feat(library/algebra): add to developments of group, ordered_group, and ring
feat(library): reorganize and declare some notation