tests(test/lean): remove 'Importing...' message, the tests using the Import command fail when running on a different machine

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

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/tactic/apply_tactic): bug in apply_tac

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/tactic/apply_tactic): allow apply_tac Lua binding to take expressions as argument

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel/normalizer): let normalizer ignore 'undefined' constants

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(util/list): improve to_list function, it takes an optional tail

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(kernel/replace_fn): ignore the cached type in constants

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(tests/kernel/environment): adjust the test to reflect (recent) change in the normalizer

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(tests/lean/tactic14.lean): typo

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/tactic/apply_tactic): improved parametric apply_tactic

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/tactic/apply_tactic): try other solutions produced by the elaborator

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lua/parser): typo

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lua/parser): allow users to specify the precedence of macros

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(memcheck.supp): another suppression for awk

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(util/lean_path): include ../library in the default LEAN_PATH

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(build): cpack support

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(build): missing file

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean/parser): add Find command

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(travis): upload Lean package to Dropbox
chore(travis): fix package name