mathlib3
fix(tactic/squeeze): do not fail when closing the goal (#2261)
#2262

Merged

fix(tactic/squeeze): do not fail when closing the goal (#2261) #2262

mergify merged 2 commits into master from squeeze-fix

fix(tactic/squeeze): do not fail when closing the goal

d8f5fc0e

cipher1024 assigned

kim-em 5 years ago

kim-em approved these changes on 2020-03-28

kim-em added ready-to-merge

Merge branch 'master' into squeeze-fix

fd5749bf

mergify merged d470ae77 into master 5 years ago

bryangingechen deleted the squeeze-fix branch 5 years ago

Reviewers

kim-em

Assignees

kim-em

Labels

ready-to-merge

Milestone

No milestone