diff options
Diffstat (limited to 'kernel/nativelambda.ml')
| -rw-r--r-- | kernel/nativelambda.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index acf1154660..8ea28ddff1 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -647,9 +647,11 @@ and lambda_of_app env sigma f args = let cb = lookup_constant kn !global_env in (try let prefix = get_const_prefix !global_env kn in + (* We delay the compilation of arguments to avoid an exponential behavior *) + let f = Retroknowledge.get_native_compiling_info + (!global_env).retroknowledge (mkConst kn) prefix in let args = lambda_of_args env sigma 0 args in - Retroknowledge.get_native_compiling_info - (!global_env).retroknowledge (mkConst kn) prefix args + f args with Not_found -> begin match cb.const_body with | Def csubst -> |