For technical reasons, we cannot easily add a warning to top-level
definitions, so 2a6e4ae49a891adc7c0562fda08b17d60beb1b4f and
e51f736076548459f36a1250de4bf6867f880b66 reverted the deprecation. But
we can still remove mention of the would-be deprecated definitions to
steer people towards using the preferred alternatives.