Unused variable in Tactic/Where

Stream: batteries

[Yaël Dillies]

When running lake build on mathlib, I get

warning: ././.lake/packages/std/././Std/Tactic/Where.lean:38:10-38:16: unused variable `simple`

Are people awhere of this?

[Kyle Miller]

It looks like this has been fixed: https://github.com/leanprover/std4/commit/3025cb124492b423070f20cf0a70636f757d117f#diff-ca48374273627f70806c17a1fa148e464684a3f8e0e81bce334069b133a327ddL38