Leonardo de Moura 54f7bf9391 fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages ... Summary: We minimize the number of "'sorry' used warning messages". We also re-target the error to the main declaration. Example: foo._main ==> foo We do not report for auxiliary declarations such as "_example" and "foo.equations._eqn_1" Get rid of the redundant error message "error : failed" for tactics. We added "silent failures" in the tactic framework. We do not store line/col information for tactics nested in notation declarations. Before this commit, we would have tactics such as (tactic.save_info line col) nested inside of notation declarations.		2017-02-07 20:25:28 -08:00
..
1313.lean	test(tests/lean/interactive): add regression test for #1313	2017-01-20 21:48:19 -08:00
1313.lean.expected.out	test(tests/lean/interactive): add regression test for #1313	2017-01-20 21:48:19 -08:00
complete.lean	fix(shell/server): prevent empty prefix completion for declarations	2017-01-17 16:38:00 -08:00
complete.lean.expected.out	fix(library,tests/lean): fix run/interactive tests, and problems in the standard library due to the new interpretation for Type	2017-01-30 11:54:00 -08:00
complete_field.lean	feat(frontends/lean,shell): autocompletion for ^.	2017-01-17 19:27:59 -08:00
complete_field.lean.expected.out	feat(frontends/lean, library/init): add 'thunk' gadget	2017-01-31 18:41:59 -08:00
complete_import.lean	feat(frontends/lean): rework and simplify completion parsing, enabling completion of empty prefixes	2017-01-10 12:25:33 +01:00
complete_import.lean.expected.out	feat(frontends/lean): rework and simplify completion parsing, enabling completion of empty prefixes	2017-01-10 12:25:33 +01:00
complete_namespace.lean	fix(frontends/lean/builtin_cmds): do not complete after namespace	2017-01-10 14:42:48 -08:00
complete_namespace.lean.expected.out	fix(frontends/lean/builtin_cmds): do not complete after namespace	2017-01-10 14:42:48 -08:00
complete_scanner_error.lean	fix(frontends/lean/parser): catch exceptions thrown by sync_command	2017-01-10 14:42:48 -08:00
complete_scanner_error.lean.expected.out	fix(frontends/lean/parser): catch exceptions thrown by sync_command	2017-01-10 14:42:48 -08:00
complete_tactic.lean	feat(frontends/lean): rework and simplify completion parsing, enabling completion of empty prefixes	2017-01-10 12:25:33 +01:00
complete_tactic.lean.expected.out	chore(tests/lean): fix tests after error-recovery	2017-02-06 15:15:47 +01:00
complete_trailing_period.lean	chore(tests/lean/interactive): simplify input format and test full completion output	2017-01-10 12:25:33 +01:00
complete_trailing_period.lean.expected.out	fix(library,tests/lean): fix run/interactive tests, and problems in the standard library due to the new interpretation for Type	2017-01-30 11:54:00 -08:00
do_info.lean	fix(frontends/lean): auxiliary bind-application in do-notation was not allowing us to obtain type information for the monadic actions.	2017-01-12 18:38:31 -08:00
do_info.lean.expected.out	fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages	2017-02-07 20:25:28 -08:00
field_info.lean	chore(tests/lean/interactive): simplify input format and test full completion output	2017-01-10 12:25:33 +01:00
field_info.lean.expected.out	fix(library/string,library/init/data/to_string): handle ASCII control characters	2017-01-11 23:44:33 -08:00
goal_info.lean	fix(frontends/lean/tactic_notation): add skip tactic to save intermediate result	2017-01-20 20:58:05 -08:00
goal_info.lean.expected.out	fix(frontends/lean/tactic_notation): add skip tactic to save intermediate result	2017-01-20 20:58:05 -08:00
info.lean	feat(frontends/lean/info_manager,shell/server,emacs/lean-type): info: provide more metadata	2017-01-11 15:29:14 +01:00
info.lean.expected.out	feat(frontends/lean, library/init): add 'thunk' gadget	2017-01-31 18:41:59 -08:00
info1.lean	chore(tests/lean/interactive): simplify input format and test full completion output	2017-01-10 12:25:33 +01:00
info1.lean.expected.out	chore(tests/lean/interactive): simplify input format and test full completion output	2017-01-10 12:25:33 +01:00
info_goal.lean	fix(frontends/lean/tactic_notation): report state after tactic execution on ,	2017-01-17 16:38:00 -08:00
info_goal.lean.expected.out	fix(frontends/lean/tactic_notation): trace messages in nested blocks were not being displayed in the correct place	2017-02-05 18:20:10 -08:00
mk_input.sh	feat(frontends/lean,library/scoped_ext,shell): complete namespaces	2017-01-10 12:25:33 +01:00
my_tac_class.lean	fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages	2017-02-07 20:25:28 -08:00
my_tac_class.lean.expected.out	fix(library/vm): make sure vm_rb_map objects can be stored in ts_vm_obj	2017-01-26 15:58:11 -08:00
nested_traces.lean	fix(frontends/lean/tactic_notation): trace messages in nested blocks were not being displayed in the correct place	2017-02-05 18:20:10 -08:00
nested_traces.lean.expected.out	fix(frontends/lean/tactic_notation): trace messages in nested blocks were not being displayed in the correct place	2017-02-05 18:20:10 -08:00
rb_map_ts.lean	fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages	2017-02-07 20:25:28 -08:00
rb_map_ts.lean.expected.out	fix(library/vm): make sure vm_rb_map objects can be stored in ts_vm_obj	2017-01-26 15:58:11 -08:00
run_single.sh	chore(tests/lean/interactive): simplify input format and test full completion output	2017-01-10 12:25:33 +01:00
sync.input	chore(tests/lean/interactive): simplify input format and test full completion output	2017-01-10 12:25:33 +01:00
sync.input.expected.out	chore(tests/lean/interactive): simplify input format and test full completion output	2017-01-10 12:25:33 +01:00
test_single.sh	feat(interactive/test_single): colorized diff	2017-02-06 15:08:45 +01:00
trace.lean	fix(library/init/meta): bug introduced 9bee8ce36d	2017-02-03 17:01:46 -08:00
trace.lean.expected.out	fix(library/init/meta): bug introduced 9bee8ce36d	2017-02-03 17:01:46 -08:00