diff options
| author | Pierre Roux | 2018-08-28 14:31:37 +0200 |
|---|---|---|
| committer | Pierre Roux | 2019-11-01 10:20:31 +0100 |
| commit | 79605dabb10e889ae998bf72c8483f095277e693 (patch) | |
| tree | fd2cf05ce8e4a2748700c7d1458a574f91dbab97 /kernel/primred.mli | |
| parent | dda50a88aab0fa0cfb74c8973b5a4353fe5c8447 (diff) | |
Change return type of primitive float comparison
Replace `option comparison` with `float_comparison` (:= `FEq | FLt |
FGt | FNotComparable`) as suggested by Guillaume Melquiond to avoid
boxing and an extra match when using primitive float comparison.
Diffstat (limited to 'kernel/primred.mli')
| -rw-r--r-- | kernel/primred.mli | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/kernel/primred.mli b/kernel/primred.mli index b2c9ebc6ea..5531c81550 100644 --- a/kernel/primred.mli +++ b/kernel/primred.mli @@ -11,7 +11,7 @@ val get_bool_constructors : env -> constructor * constructor val get_carry_constructors : env -> constructor * constructor val get_pair_constructor : env -> constructor val get_cmp_constructors : env -> constructor * constructor * constructor -val get_option_constructors : env -> constructor * constructor +val get_f_cmp_constructors : env -> constructor * constructor * constructor * constructor exception NativeDestKO (* Should be raised by get_* functions on failure *) @@ -33,8 +33,10 @@ module type RedNativeEntries = val mkLt : env -> elem val mkEq : env -> elem val mkGt : env -> elem - val mkSomeCmp : env -> elem -> elem - val mkNoneCmp : env -> elem + val mkFLt : env -> elem + val mkFEq : env -> elem + val mkFGt : env -> elem + val mkFNotComparable : env -> elem end module type RedNative = |