vpx_timer.h uses several defines from the config file including
CONFIG_OS_SUPPORT and INLINE

Change-Id: I16cb45237787cbc1ae79a67e16b8042811dda336