Require Reals. 
Extract Inlined Constant R => float.
Extract Inlined Constant R0 => "0.0".
Extract Inlined Constant R1 => "1.0".
Extract Inlined Constant Rplus => "(+.)".
Extract Inlined Constant Rmult => "( *.)".
Extract Inlined Constant Ropp => "(~-.)".
Extract Inlined Constant Rinv => "(fun x -> 1.0 /. x)".
Extract Inlined Constant Rlt => "(<)".
Extract Inlined Constant up => "AddReals.my_ceil".
Extract Inlined Constant total_order_T => "AddReals.total_order_T".