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

Commit

5 years ago

fix(tactic/squeeze): do not fail when closing the goal (#2262) Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

References

Author

cipher1024

Parents