diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2014-04-08 20:42:46 -0400 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2014-04-09 01:05:48 -0400 |
| commit | 43fbb57e7982c028ee0c74b0252f24fef29a68a4 (patch) | |
| tree | ec16018c2726b025d5573e83a8f8c10517ecd63f /kernel/nativecode.ml | |
| parent | d356af7f7d8601f4897978587429297d05a934ce (diff) | |
Optimizing Int31 support in native compiler, by not tagging
applications of I31 constructor as lazy.
Diffstat (limited to 'kernel/nativecode.ml')
| -rw-r--r-- | kernel/nativecode.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index c8572eec3..2cbe9cd22 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 |