From 73580b9c5f206e2d3a7107123d207515f2330978 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Tue, 23 Oct 2018 17:52:39 +0200
Subject: 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.
---
 kernel/nativelambda.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel/nativelambda.mli')

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
-- 
cgit v1.2.3