Question regarding type ee_f32

[TerrenceZhangX]

Hello, I noticed that type ee_f32 is defined as double in core_portme.h, but double represents 64bits in both rv32 and rv64 per riscv-spec: https://riscv.org/wp-content/uploads/2015/01/riscv-calling.pdf.
Could you help me understand why the definition is like this? Thank you 🤓

coremark/barebones/core_portme.h

Line 90 in eefc986

typedef double ee_f32;