Rather than add the FIXME I owe you, I figured I'd fix at least most of
the (potential) problem.  This patch corrects explicit references to
registers to use the known IEEE floating-point types instead of
builtin_type_{float,double}.

OK?

-- 
Daniel Jacobowitz                           Carnegie Mellon University
MontaVista Software                         Debian GNU/Linux Developer