syst_float128_to_float64
float64 syst_float128_to_float64( float128 );
float128_to_float64, syst_float128_to_float64 );