Add minimal syntactic support for type _Float16

[xavierleroy]

Appendix H of ISO C 2023 makes provisions for built-in binary floating-point types _FloatN, where N is the bit size of the type.

Some C compilers and math libraries already make use of type _Float16 to denote half-precision FP numbers. That's the case for XCode 16 on macOS 15, which declares _Float16 functions in <math.h> without guarding them with a #ifdef, e.g.

extern _Float16 __fabsf16(_Float16) __API_AVAILABLE(macos(15.0), ios(18.0), watchos(11.0), tvos(18.0));

With the current CompCert, any C source code that includes <math.h> causes a syntax error on these declarations.

This PR proposes to add minimal syntactic support for type _Float16. It is kept as a distinct FP type during elaboration, then rejected during conversion to CompCert C. This way, _Float16 functions declared in header files but not used in the C source file are silently ignored. If these functions are used, an "unsupported feature" error is reported.

The verified part of CompCert is unchanged.

[xavierleroy]

A first cut of this PR also added _Float32 and _Float64 as synonymous for float and double, but this causes problems with Glibc header files, and is not needed.

[xavierleroy]

Thanks for the feedback and testing. Merging!