mathlib3
fix(tactic/h_generalize): fix name resolution in h_generalize
#688

Merged

fix(tactic/h_generalize): fix name resolution in h_generalize #688

cipher1024 merged 1 commit into master from fix-h_generalize-name-resolution

fix(tactic/h_generalize): fix name resolution in h_generalize

ff5af101

cipher1024 merged 9f79d2eb into master 6 years ago

johoelzl deleted the fix-h_generalize-name-resolution branch 6 years ago

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Milestone

No milestone