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 /vernac | |
| 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 'vernac')
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index ec32c83670..c86b70c78e 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1847,7 +1847,7 @@ let vernac_register qid r = | "ind_carry" -> CPrimitives.(PIE PIT_carry) | "ind_pair" -> CPrimitives.(PIE PIT_pair) | "ind_cmp" -> CPrimitives.(PIE PIT_cmp) - | "ind_option" -> CPrimitives.(PIE PIT_option) + | "ind_f_cmp" -> CPrimitives.(PIE PIT_f_cmp) | k -> CErrors.user_err Pp.(str "Register: unknown identifier “" ++ str k ++ str "” in the “kernel” namespace") in match gr with |