OK, I removed all comments that could have conceivably come from somewhere else originally in my latest commit to this pull request.  Perhaps we can create a different pull request to remove all such comments from core.stdc.