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 /pretyping/nativenorm.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 'pretyping/nativenorm.ml')
| -rw-r--r-- | pretyping/nativenorm.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index e5aed300a2..0178d5c009 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -208,6 +208,7 @@ let rec nf_val env sigma v typ = mkLambda(name,dom,body) | Vconst n -> construct_of_constr_const env sigma n typ | Vint64 i -> i |> Uint63.of_int64 |> mkInt + | Vfloat64 f -> f |> Float64.of_float |> mkFloat | Vblock b -> let capp,ctyp = construct_of_constr_block env sigma (block_tag b) typ in let args = nf_bargs env sigma b ctyp in |