diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/byterun/coq_interp.c | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index e67325eb9a..6e6adb1293 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -1652,6 +1652,12 @@ value coq_interprete double f; print_instr("CHECKFRSHIFTEXP"); CheckFloat1(); + /* frexp(infinity) incorrectly returns nan on mingw */ +#if defined(__MINGW32__) || defined(__MINGW64__) + if (fpclassify(Double_val(accu)) == FP_INFINITE) { + f = Double_val(accu); + } else +#endif f = frexp(Double_val(accu), &exp); if (fpclassify(f) == FP_NORMAL) { exp += FLOAT_EXP_SHIFT; |