mathlib3
fix(tactic/{use,ring}): instantiate metavariables in goal
#1520

Merged

fix(tactic/{use,ring}): instantiate metavariables in goal #1520

mergify merged 4 commits into master from use

fix(tactic/{use,ring}): instantiate metavariables in goal

a47d7da2

robertylewis added awaiting-review

digama0 approved these changes on 2019-10-08

robertylewis removed awaiting-review

robertylewis added ready-to-merge

Merge branch 'master' into use

fb6cfe4f

Merge branch 'master' into use

46f8eacf

Merge branch 'master' into use

d833c74a

mergify merged a17a9a6a into master 6 years ago

mergify deleted the use branch 6 years ago

Reviewers

digama0

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone