mathlib3
fix(tactic/squeeze): make suggestion at correct location
#2279

Merged

fix(tactic/squeeze): make suggestion at correct location #2279

mergify merged 2 commits into master from squeeze_pos

fix(tactic/squeeze): make suggestion at correct location

3327dfa0

gebner added awaiting-review

cipher1024 approved these changes on 2020-03-29

cipher1024 removed awaiting-review

cipher1024 added ready-to-merge

Merge branch 'master' into squeeze_pos

28314eaf

mergify merged 8b679d98 into master 6 years ago

bryangingechen deleted the squeeze_pos branch 6 years ago

Reviewers

cipher1024

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone