diff --git a/include/arch/arm/arch/object/vcpu.h b/include/arch/arm/arch/object/vcpu.h
index f21f39ba1..cc9ac5e94 100644
--- a/include/arch/arm/arch/object/vcpu.h
+++ b/include/arch/arm/arch/object/vcpu.h
@@ -204,7 +204,6 @@ static inline VPPIEventIRQ_t irqVPPIEventIndex(irq_t irq)
 
 #else /* end of CONFIG_ARM_HYPERVISOR_SUPPORT */
 
-/* used in boot.c with a guard, use a marco to avoid exposing vcpu_t */
 #define vcpu_boot_init() do {} while(0)
 #define vcpu_switch(x) do {} while(0)
 static inline void VGICMaintenance(void) {}