mathlib3
3ae44bd1 - fix(tactic/equiv_rw): fix problem with stuck universe metavariables (#3773)

Commit

5 years ago

fix(tactic/equiv_rw): fix problem with stuck universe metavariables (#3773) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author

kim-em

Parents