aboutsummaryrefslogtreecommitdiff
path: root/kernel/cemitcodes.ml
diff options
context:
space:
mode:
authorPierre Roux2018-08-28 18:56:07 +0200
committerPierre Roux2019-11-01 10:20:35 +0100
commitd18b928154a48ff8d90aaff69eca7d6eb3dfa0ab (patch)
tree9cc9b39b16849ed839f4adf7b19e3d3291f7dd98 /kernel/cemitcodes.ml
parent79605dabb10e889ae998bf72c8483f095277e693 (diff)
Implement classify on primitive float
Diffstat (limited to 'kernel/cemitcodes.ml')
-rw-r--r--kernel/cemitcodes.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 82dd7bd85d..535034d8fa 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -237,6 +237,7 @@ let check_prim_op = function
| Float64opp -> opCHECKOPPFLOAT
| Float64abs -> opCHECKABSFLOAT
| Float64compare -> opCHECKCOMPAREFLOAT
+ | Float64classify -> opCHECKCLASSIFYFLOAT
| Float64add -> opCHECKADDFLOAT
| Float64sub -> opCHECKSUBFLOAT
| Float64mul -> opCHECKMULFLOAT