-
Richard Eisenberg authored
This reverts commit 3a51abd0. I had hit the wrong button when trying to validate the original commit... and ended up committing it prematurely instead. This reversion commit also updates the comments to explain why we kind-generalise.
09740d50