fix(library/unifier): broken optimization in the unifier

See new comments and tests for details.
fix(library/tactic/goal): avoid unnecessary line break when possible
feat(library/tactic/goal): add option `pp.compact_goals`
feat(frontends/lean/info_manager): add separator `--` when displaying PROOF_STATE info

This feature was implemented to address issue #259
chore(README.md): add 'issue stat' badges
feat(frontends/lean): modify `begin-end` semantics, closes #258
feat(frontends/lean): hide tactic "types"

it is not very useful to display the type of tactics (e.g., apply,
intros, ...)
feat(library/tactic): add whnf tactic, closes #270
fix(frontends/lean): squiggle position for unary begin-end block
fix(library/tactic): add relax_main_opaque flag to proof_state objects, closes #274
feat(library/definitional/projection): add projection generator, closes #257
fix(library/definitional/projection): error messages for projection generation
feat(emacs/lean-input): add lean-input-export-translations
feat(emacs/lean-info): add PROOF_STATE info

Close #259
feat(emacs): extract proof state information attached to ","
feat(emacs/lean-settings): add lean-show-proofstate-in-minibuffer option
feat(emacs/lean-type): output INFO to *lean-info* buffer in addition to minibuffer

Close #260
fix(emacs/lean-syntax): fix Type1, Type2 highlight
feat(emacs/lean-mode): add lean-info-mode for "*lean-info*" buffer
test(emacs/lean-info-test): add test for proofstate info