Javadoc errors

[Julian Hyde]

Jesus' last commit had some javadoc errors ("mvn javadoc:javadoc
javadoc:test-javadoc" under JDK 1.9). I am fixing them and will commit
shortly.