It's not misleading in this case. It's used in practice. You have to understand that CompCert's main competition in this space was an ancient version of GCC wi

It's not misleading in this case. It's used in practice. You have to understand that CompCert's main competition in this space was an ancient version of GCC without any optimizations. This is mostly an issue of certification. CompCert got the same certification and is already a great improvement just by virtue of having a register allocator...