feat(src/emacs/lean-mode): add shortcut for restarting lean server
refactor(frontends/lean): combine info annotations in a single module
fix(frontends/lean): type information for "atomic" notation declaration, fixes #292
refactor(frontends/lean/local_context): add 'const' modifier
fix(frontends/lean/placeholder_elaborator): local context must be adjusted when performing class-instance resolution modulo Pi-abstraction, fixes #293
fix(library/hott) fix funext.lean by making funext an instance
chore(library/hott) move theorem about precomposition to its own file
feat(library/hott) add theorem: assuming function extensionality, precomposing and postcomposing of equivalences is an equivalence
fix(frontends/lean/structure_cmd): universe level validation