mathlib3
fix(tactic/core): remove all_goals option from apply_any
#2275

Merged

fix(tactic/core): remove all_goals option from apply_any #2275

mergify merged 3 commits into master from solve_by_elim_bug

fix(tactic/core): remove all_goals option from any_apply

4c8d3d6f

remove unnecessary imports

dbcb5b46

kim-em added bug

kim-em added t-meta

kim-em requested a review from

cipher1024 6 years ago

kim-em requested a review from

gebner 6 years ago

kim-em requested a review from

kbuzzard 6 years ago

bryangingechen changed the title ~~fix(tactic/core): remove all_goals option from any_apply~~ fix(tactic/core): remove all_goals option from apply_any 6 years ago

bryangingechen approved these changes on 2020-03-29

bryangingechen added ready-to-merge

Merge branch 'master' into solve_by_elim_bug

3eb36921

mergify merged c4fb4035 into master 6 years ago

bryangingechen deleted the solve_by_elim_bug branch 6 years ago

Reviewers

bryangingechen

cipher1024

gebner

kbuzzard

Assignees

No one assigned

Labels

bug ready-to-merge t-meta

Milestone

No milestone

mathlib3 fix(tactic/core): remove all_goals option from apply_any #2275 Merged

fix(tactic/core): remove all_goals option from apply_any #2275

mathlib3
fix(tactic/core): remove all_goals option from apply_any
#2275

Merged