Make sure files defined to include mini header really include the mini header

[houshengbo]

Some files have already included full header, but we can leave them as they are for the first release.
For further releases, we may change them based on what we designate them to be.

[dgrove-oss]

obsolete; we are using full headers in all files.