fix(frontends/lean/builtin_cmds): allow coercion command inside section, fixes #186
fix(library/coercion): remove spurious '\n'
feat(library/coercion): better support for coercions to function-class. closes #185
refactor(emacs/debug): rename lean-server-debug to lean-debug
refactor(emacs/lean-server): rename flush-changed-lines to server-flush-changed-lines
feat(emacs/lean-changes): handle before/after-revert
fix(frontends/lean/elaborator): remove annotation left-over
fix(util/lazy_list): bug in filter operation
fix(frontends/lean/placeholder_elaborator): do not truncate stream of
solutions during class-instance resolution, closes #183

For example, in theorem inverse_unique at category.lean, implicit
arguments are synthesized for inverse_compose. The first solution H' is
not good, and produces a type incorrect solution
fix(frontends/lean/server): std::unordered_map::insert does replace
existing entry, fixes #188
refactor(frontends/lean/elaborator): do not save/restore cache
feat(frontends/lean/elaborator): cleanup and remove unnecessary code
feat(frontends/lean/elaborator): constraints associated with 'proof-qed'
blocks are solved independently, closes #82
chore(emacs/README.md): add 'f' as a required package for lean-mode
fix(bin/linja): show ninja error/warning
feat(emacs/lean-company): auto-completion for import

Close #126
feat(src/cmake/modules/CleanOlean.cmake): add CleanOlean.cmake

Instead of using 'find -delete', use CMAKE's FILE GLOB_RECURSE and FILE
REMOVE to implement clean-olean.

Related issue: #166
chore(library/coercion): cleanup
feat(frontends/lean): allow multiple coercions from class A to B, closes #187

See new tests (for examples)
tests/lean/run/coe10.lean
tests/lean/run/coe11.lean
tests/lean/run/coe9.lean

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/error_handling): generate valid line and column information
when in flycheck mode