I have no idea about this specific case, but this kind of claim can be very misleading, while remaining true. Maybe they used the tooling once for an offline script of some sort, and that is all.
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...
A register allocator! :)