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 /plugins/syntax/float_syntax.ml | |
| 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 'plugins/syntax/float_syntax.ml')
0 files changed, 0 insertions, 0 deletions