feat(shell/lean): add '--server-trace' flag, closes #264
fix(frontends/lean/elaborator): remove invalid assertions

These assertions became invalid when we changed the behavior of undef
indentifiers at

https://github.com/leanprover/lean/commit/8e6de933948748b26ff685bedb76f3e691df9e36
feat(kernel/type_checker): add `is_stuck` method, and improve ensure_pi method, closes #261
feat(library/normalize): add new flavors of normalize procedure
feat(library/unifier): improve FailLocal/FailCircular failures in the unifier by using normalization

This improvements was marked as TODO, and was preventing us from
elaborating the example in the new test vector3.lean
fix(frontends/lean): `begin-end` automatic tactic notation bug, fixes #262
fix(kernel/inductive): relax eliminator generation rules for empty types

This commit also removes the workaround false.rec_type. It is not needed anymore
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