diff options
Diffstat (limited to 'backend/RTLgen.v')
| -rw-r--r-- | backend/RTLgen.v | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/backend/RTLgen.v b/backend/RTLgen.v index 65e873e8..39add986 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -630,9 +630,7 @@ Definition transl_function (f: CminorSel.function) : Errors.res RTL.function := rparams f.(CminorSel.fn_stackspace) s.(st_code) - nentry - s.(st_nextnode) - s.(st_wf)) + nentry) end. Definition transl_fundef := transf_partial_fundef transl_function. |