mathlib3
[Merged by Bors] - fix(tactic/interval_cases): instantiate metavars
#19232

Closed

[Merged by Bors] - fix(tactic/interval_cases): instantiate metavars #19232

eric-wieser wants to merge 1 commit into master from eric-wieser/interval_cases-mvars-fix

fix: instatiate metavars in interval_cases

85e6df66

eric-wieser added awaiting-review

eric-wieser added awaiting-CI

eric-wieser requested a review 2 years ago

eric-wieser added t-meta

eric-wieser changed the title ~~fix: instatiate metavars in interval_cases~~ fix(tactic/interval_cases): instantiate metavars 2 years ago

kmill approved these changes on 2023-07-11

leanprover-community-bot-assistant added delegated

leanprover-community-bot-assistant removed awaiting-review

github-actions removed awaiting-CI

github-actions added ready-to-merge

bors changed the title ~~fix(tactic/interval_cases): instantiate metavars~~ [Merged by Bors] - fix(tactic/interval_cases): instantiate metavars 2 years ago

bors closed this 2 years ago

bors deleted the eric-wieser/interval_cases-mvars-fix branch 2 years ago

Reviewers

kmill

Assignees

No one assigned

Labels

ready-to-merge t-meta delegated

Milestone

No milestone

mathlib3 [Merged by Bors] - fix(tactic/interval_cases): instantiate metavars #19232 Closed

[Merged by Bors] - fix(tactic/interval_cases): instantiate metavars #19232

mathlib3
[Merged by Bors] - fix(tactic/interval_cases): instantiate metavars
#19232

Closed