diff options
| author | Pierre Roux | 2018-08-28 18:56:07 +0200 |
|---|---|---|
| committer | Pierre Roux | 2019-11-01 10:20:35 +0100 |
| commit | d18b928154a48ff8d90aaff69eca7d6eb3dfa0ab (patch) | |
| tree | 9cc9b39b16849ed839f4adf7b19e3d3291f7dd98 /kernel/cPrimitives.mli | |
| parent | 79605dabb10e889ae998bf72c8483f095277e693 (diff) | |
Implement classify on primitive float
Diffstat (limited to 'kernel/cPrimitives.mli')
| -rw-r--r-- | kernel/cPrimitives.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli index 3e6ec8dbcc..af95f6c6d7 100644 --- a/kernel/cPrimitives.mli +++ b/kernel/cPrimitives.mli @@ -36,6 +36,7 @@ type t = | Float64opp | Float64abs | Float64compare + | Float64classify | Float64add | Float64sub | Float64mul @@ -75,6 +76,7 @@ type 'a prim_ind = | PIT_pair : (prim_type * prim_type) prim_ind | PIT_cmp : unit prim_ind | PIT_f_cmp : unit prim_ind + | PIT_f_class : unit prim_ind type prim_ind_ex = PIE : 'a prim_ind -> prim_ind_ex |