fix(emacs/lean-info): fix eldoc-error at end of buffer
feat(frontends/lean): remove restriction on implict arguments, add new test that demonstrates the new feature

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(emacs/lean-company): add company-lean--need-autocomplete

This one partially addresses #150.
feat(frontends/lean): add [class] modifier for inductive datatypes as a shortcut for 'class' command.
feat(frontends/lean/elaborator): allow Pi/forall local instances
chore(emacs/lean-info): fix a bug passing a wrong argument
fix(frontends/lean/elaborator): bug in recent change
feat(library/data/vector): add vec.is_inhabited theorem
feat(library/classes/inhabited): add dfun_inhabited theorem
fix(emacs/lean-server): use process-query-on-exit-flag to kill
lean-server automatically on exit

To fix a problem mentioned in #147
feat(library/data/nat): add nat.is_inhabited theorem
fix(library/scoped_ext): section/context should not affect namespace
feat(frontends/lean/elaborator): (Pi/forall) intro in class inference, closes #77