diff options
Diffstat (limited to 'kernel/float64.mli')
| -rw-r--r-- | kernel/float64.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/float64.mli b/kernel/float64.mli index 7ced535dc0..c82f1d84da 100644 --- a/kernel/float64.mli +++ b/kernel/float64.mli @@ -24,7 +24,7 @@ val of_float : float -> t val opp : t -> t val abs : t -> t -type float_comparison = Eq | Lt | Gt | NotComparable +type float_comparison = FEq | FLt | FGt | FNotComparable (** The IEEE 754 float comparison. * NotComparable is returned if there is a NaN in the arguments *) |