The files in platform/*/include are merged with the files in
cpu/*/include to become the <machine/*.h> include files. Header
files in platform/*/include override the ones in cpu/*/include.
The cpu/*/include header files are also available via <cpu/*.h>.
Use of #include <cpu/*.h> should ONLY EVER be done by platform
header files, never by anyone else. This abstraction exists simply
to allow platform header files to extend cpu header files. For
example, look at "platform/vkernel/include/types.h".
-Matt
