subgroup warning

Stream: general

[Patrick Massot]

Does anyone get a message on line 250 of subgroup.lean?

[Patrick Massot]

I tried to rebase an old WIP on current master and I'm seeing that. I had to resolve a bunch of conflicts but I'm sure I didn't touch that file.

[Yury G. Kudryashov]

I'll fix it tonight.

[Yury G. Kudryashov]

And replace a warning with something more understandable.

[Yury G. Kudryashov]

It tries to say that to_additive autogenerates the same name as the one given in the argument, so "of_sub" can be safely removed.