feat(library/tactic/generalize): add 'generalizes' syntax sugar, closes #327
refactor(library/data/nat/div): remove unnecessary annotations
feat(frontends/lean/placeholder_elaborator): apply substitution before collecting local instances, closes #333
feat(frontends/lean): allow user to associate precedence to binders, closes #323
feat(library/hott) change axioms to Leo's axioms-as-typeclass proposal
chore(library/hott) adapted theories to typeclass axioms
fix(library/hott) fill both gaps (I don't know why it works that way), change name from funext.apply to funext.ap, since apply seems to be a tactic name?
chore(library/hott) adjust funext_from_ua.lea to typeclass axioms
fix(library/hott) fix equiv_precomp, doesn't look nice now
chore(library/hott) make funext more general
feat(library/hott) funext from ua now with arbitrary universe levels for funext!
chore(library/hott) made ua_implies_funext a class instance
fix(frontends/lean/parser_config): binder(s) rbp was not being saved in .olean file
feat(frontends/lean/server): do not unfold definitions in FINDG
feat(frontends/lean): add 'find_decl' command
feat(frontends/lean/find_cmd): add options for controlling find_decl
fix(emacs/lean-flycheck): fix bug in advice for lean-flycheck-try-parse-error-with-pattern

I provided an "advice" for 'flycheck-try-parse-error-with-pattern'
function to change its behavior, namely to increase error-columns by
one.

Bug
===

The problem is that it doesn't consider the case where the pattern is
not matched and ends up with "err = nil". For this case,
"(flycheck-error-column err)" generates an exception if executed. The
whole error parsing process stops immediately.

This causes a problem when we have more than one error-patterns, which
is the case when we enable 'error' and 'warning' patterns.

Fix
===

Fix is simple: check err before executing (flycheck-error-column err)

-            (col (flycheck-error-column err)))
+            (col (and err (flycheck-error-column err))))