fix(library/unifier): bug in unifier priority queue

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean/elaborator): case-split on coercions that cannot be resolved by postponing

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): try overloaded notation and declarations in the order they were defined

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): change the name resolution rules: when in a namespace N that defines C, then C always refers to N.C (i.e., it overrides any alias)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(emacs): add company mode (via etags)
feat(emacs/lean): add multi-line comments

This is related with issue #63.

There are two known issues:

 - Emacs behaves as if the multi-line comment start/end symols are "(-"
   and "-)" instead of "(--" and "--)". As a result, it shows all the
   correct lean comments as it is. However, it will show some examples
   such as "(-5)" as a part of comment even if Lean doesn't interpret it
   as it is. Technically, it's because we are using a syntax-table based
   method to define comments. For more information read a documentation
   of 'modify-syntax-entry' function.

 - Somehow, the matching parens are broken. When we type "--)" to close
   a multi-line comment. Emacs warns "Mismatched Parentheses".
checkpoint