feat(frontends/parser): improve error message when an apply tactic refers a local constant that is not marked as [fact]

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/tactic/goal): propagate tag (for position information) from goal to subgoal

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(frontends/lean): remove unnecessary code

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(kernel/metavar): add method instantiate as alias for instantiate_metavars_wo_jst

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean/elaborator): report unassigned metavariables as goals

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(frontends/lean): code cleanup

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean/elaborator): instantiate metavariables before displaying error message

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/tactic): rename 'exact' to 'assumption', 'exact' is a different tactic

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/tactic): add 'exact' tactic

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(emacs): update emacs mode

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean/elaborator) add trick for improving error messages when mixing tactics, elaboration and exact tactic

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>