Commit c9cf7d64 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan Committed by Guillaume Melquiond

Fix division by infinity.

parent 6c0480f2
......@@ -1412,7 +1412,7 @@ Definition Bdiv m x y :=
| _, B754_nan => y
| B754_infinity sx, B754_infinity sy => B754_nan
| B754_infinity sx, B754_finite sy _ _ _ => B754_infinity (xorb sx sy)
| B754_finite sx _ _ _, B754_infinity sy => B754_infinity (xorb sx sy)
| B754_finite sx _ _ _, B754_infinity sy => B754_zero (xorb sx sy)
| B754_infinity sx, B754_zero sy => B754_infinity (xorb sx sy)
| B754_zero sx, B754_infinity sy => B754_zero (xorb sx sy)
| B754_finite sx _ _ _, B754_zero sy => B754_infinity (xorb sx sy)
......
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