[records] Summary so far

[Jonathan Gibbons]

On 2/18/20 7:19 AM, Gavin Bierman wrote:
> Q6. @deprecated
>
>      Should we allow record components to be marked as @deprecated?
>
>      A: We don't want to add any additional support for @deprecated beyond the
>      fact that it is an annotation and it can be inspected via reflection.

The wording here could be improved.

`@deprecated` is a standard javadoc tag. It is not an annotation.  It 
goes along
with the @Deprecated annotation.

We should support the annotation, and support the tag in documentation as an
adjunct to the annotation, but the tag alone should not imply deprecation.
In the context of records, neither the annotation nor the tag should 
imply the
`Deprecated` attribute in the class file.

--Jon