diff options
Diffstat (limited to 'backend/Inlining.v')
| -rw-r--r-- | backend/Inlining.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/backend/Inlining.v b/backend/Inlining.v index 3e357ab0..0e18d38e 100644 --- a/backend/Inlining.v +++ b/backend/Inlining.v @@ -454,8 +454,7 @@ Definition transf_function (fenv: funenv) (f: function) : Errors.res function := (sregs ctx f.(fn_params)) s.(st_stksize) s.(st_code) - (spc ctx f.(fn_entrypoint)) - (mkuntrustedanalysis None None)) + (spc ctx f.(fn_entrypoint))) else Error(msg "Inlining: stack too big"). |