From 43fbb57e7982c028ee0c74b0252f24fef29a68a4 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 8 Apr 2014 20:42:46 -0400
Subject: Optimizing Int31 support in native compiler, by not tagging
 applications of I31 constructor as lazy.

---
 kernel/nativecode.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/nativecode.ml')

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index c8572eec3b..2cbe9cd22d 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1767,7 +1767,7 @@ let compile_constant env sigma prefix ~interactive con body =
   | Def t ->
       let t = Mod_subst.force_constr t in
       let code = lambda_of_constr env sigma t in
-      let is_lazy = is_lazy t in
+      let is_lazy = is_lazy prefix t in
       let code = if is_lazy then mk_lazy code else code in
       let name =
         if interactive then LinkedInteractive prefix
-- 
cgit v1.2.3