Commit ec99901a authored by Guillaume Melquiond's avatar Guillaume Melquiond

Remove unused function F.round.

parent 56bee29c
......@@ -60,7 +60,6 @@ Module GenericFloat (Rad : Radix) <: FloatOps.
Definition cmp (x y : type) := match Fcmp x y with Xlt => Lt | Xgt => Gt | _ => Eq end.
Definition min := @Fmin radix.
Definition max := @Fmax radix.
Definition round := @Fround radix.
Definition neg := @Fneg radix.
Definition abs := @Fabs radix.
Definition scale := @Fscale radix.
......
......@@ -57,7 +57,6 @@ Parameter mag : type -> sfactor.
Parameter cmp : type -> type -> comparison.
Parameter min : type -> type -> type.
Parameter max : type -> type -> type.
Parameter round : rounding_mode -> precision -> type -> type.
Parameter neg : type -> type.
Parameter abs : type -> type.
Parameter scale : type -> sfactor -> type.
......
......@@ -770,16 +770,6 @@ rewrite (proj1 (mantissa_one_correct)).
now rewrite Pplus_one_succ_r.
Qed.
Definition round mode prec (f : type) :=
match f with
| Float m e =>
match mantissa_sign m with
| Mzero => zero
| Mnumber s p => round_aux mode prec s p e pos_Eq
end
| _ => f
end.
(*
* mul
*)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment