diff options
| author | Pierre Roux | 2018-10-23 17:52:39 +0200 |
|---|---|---|
| committer | Pierre Roux | 2019-11-01 10:20:43 +0100 |
| commit | 73580b9c5f206e2d3a7107123d207515f2330978 (patch) | |
| tree | 6a39aacd27992c59140cc91b6a40058f469ac41f /kernel/nativelambda.mli | |
| parent | 5f1270242f71a0a1da7c868967e1071d28ed83fb (diff) | |
Add primitive floats to 'native_compute'
* Float added to is_value/get_value to avoid stack overflows
(cf. #7646)
* beware of the use of Array.map with floats (cf. comment in the
makeblock function)
NB: From here one, the configure option "-native-compiler no"
is no longer needed.
Diffstat (limited to 'kernel/nativelambda.mli')
| -rw-r--r-- | kernel/nativelambda.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index f17339f84d..1d7bf5343a 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -38,6 +38,7 @@ type lambda = (* prefix, inductive name, constructor tag, arguments *) (* A fully applied non-constant constructor *) | Luint of Uint63.t + | Lfloat of Float64.t | Lval of Nativevalues.t | Lsort of Sorts.t | Lind of prefix * pinductive |