mathlib3
feat(tactic/squeeze_simp): better handling of private declarations
#1498

Merged

feat(tactic/squeeze_simp): better handling of private declarations #1498

mergify merged 3 commits into master from squeeze_simp_privates

feat(tactic/squeeze_simp): better handling of private declarations

1e253ae1

cipher1024 requested a review 6 years ago

robertylewis commented on 2019-10-01

Update core.lean

b11bd8a4

robertylewis approved these changes on 2019-10-03

robertylewis added ready-to-merge

Merge branch 'master' into squeeze_simp_privates

574dd2e5

mergify merged f8543711 into master 6 years ago

mergify deleted the squeeze_simp_privates branch 6 years ago

Reviewers

robertylewis

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone