Leonardo de Moura f7fe2a775c feat(library/init/meta/rewrite_tactic): improve rewrite tactic ... `rewrite` tactic improvements - Add support for `auto_param` and `opt_param` - Order new goals using the same strategies available for `apply` - Allow user to set configuration object in interactive mode. @Armael This commit should address the issue you raised about the order of new goals in the `rewrite` tactic. See new test tests/lean/run/rw1.lean for examples.		2017-06-30 12:03:27 -07:00
..
1313.lean
1313.lean.expected.out
complete.lean	feat(frontends/lean/{builtin_cmds,interactive}): complete namespace/section after end	2017-04-23 11:26:31 -07:00
complete.lean.expected.out	chore(tests/lean/interactive): fix tests	2017-06-15 10:56:09 -07:00
complete_field.lean
complete_field.lean.expected.out	chore(tests/lean/interactive/complete_field): fix test	2017-05-27 10:18:44 -07:00
complete_import.lean
complete_import.lean.expected.out	fix(frontends/lean/parser): show exception message in import errors	2017-04-27 16:04:18 -07:00
complete_namespace.lean
complete_namespace.lean.expected.out
complete_scanner_error.lean
complete_scanner_error.lean.expected.out
complete_tactic.lean
complete_tactic.lean.expected.out	feat(library/compiler/eta_expansion): also eta-expand expressions containing sorry	2017-05-23 11:14:31 -07:00
complete_trailing_period.lean
complete_trailing_period.lean.expected.out
correct_snapshot_invalidation.input
correct_snapshot_invalidation.input.expected.out	chore(tests): update tests with changes to error recovery	2017-05-23 11:14:30 -07:00
do_info.lean
do_info.lean.expected.out
field_info.lean
field_info.lean.expected.out	chore(tests): fix tests	2017-06-18 18:33:38 -07:00
focus.lean
focus.lean.expected.out	feat(frontends/lean/tactic_notation): add support for tac ; [tac_1, ..., tac_n] notation in interactive tactic mode	2017-06-02 11:38:04 -07:00
goal_info.lean
goal_info.lean.expected.out
goal_info_rw.lean
goal_info_rw.lean.expected.out	feat(library/init/meta/rewrite_tactic): improve rewrite tactic	2017-06-30 12:03:27 -07:00
hole1.lean	feat(shell/server,frontends/lean): add "hole_commands" server command	2017-06-14 22:16:34 -07:00
hole1.lean.expected.out	fix(frontends/lean/interactive): revert hole end column	2017-06-15 17:01:10 +02:00
hole2.lean	feat(shell/server,frontends/lean): add "hole_commands" server command	2017-06-14 22:16:34 -07:00
hole2.lean.expected.out	fix(frontends/lean/interactive): revert hole end column	2017-06-15 17:01:10 +02:00
hole3.lean	feat(frontends/lean/info_manager): multi-line holes	2017-06-15 07:23:06 -07:00
hole3.lean.expected.out	feat(frontends/lean/info_manager): multi-line holes	2017-06-15 07:23:06 -07:00
hole4.lean	feat(frontends/lean): add option for pretty printing metavars, sorry and delayed abstractions as holes	2017-06-15 10:24:26 -07:00
hole4.lean.expected.out	chore(tests/lean/interactive): fix tests	2017-06-15 10:56:09 -07:00
info.lean
info.lean.expected.out	chore(tests/lean/interactive): fix tests	2017-06-15 10:56:09 -07:00
info1.lean
info1.lean.expected.out
info_goal.lean
info_goal.lean.expected.out
info_id_pre_elab.lean
info_id_pre_elab.lean.expected.out	chore(tests/lean/interactive): fix tests	2017-06-15 10:56:09 -07:00
info_tactic.lean	fix(frontends/lean/interactive): fall back to elaborator info when not an interactive tactic	2017-04-23 11:26:31 -07:00
info_tactic.lean.expected.out	refactor(library/init/meta/converter): new conv monad implementation	2017-06-29 16:37:22 -07:00
mk_input.sh	fix(tests/lean/interactive/mk_input): strip \r from input files (win)	2017-06-21 08:53:11 +02:00
my_tac_class.lean	fix(tests/*): fix tests	2017-06-22 08:24:19 -07:00
my_tac_class.lean.expected.out
nested_traces.lean
nested_traces.lean.expected.out
rb_map_ts.lean	fix(tests/*): fix tests	2017-06-22 08:24:19 -07:00
rb_map_ts.lean.expected.out	chore(tests/lean/interactive): fix tests	2017-06-15 10:56:09 -07:00
run_single.sh	fix(util/stackinfo): avoid and guard against negative overflow in g_stack_threshold computation	2017-06-07 13:22:11 +02:00
sync.input
sync.input.expected.out
test_single.sh
trace.lean
trace.lean.expected.out