diff options
Diffstat (limited to 'backend/Stacking.v')
| -rw-r--r-- | backend/Stacking.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/Stacking.v b/backend/Stacking.v index caf0ae59..ef96e4b3 100644 --- a/backend/Stacking.v +++ b/backend/Stacking.v @@ -146,8 +146,8 @@ Fixpoint transl_builtin_arg (fe: frame_env) (a: builtin_arg loc) : builtin_arg m BA_addrstack (Int.add ofs (Int.repr fe.(fe_stack_data))) | BA_loadglobal chunk id ofs => BA_loadglobal chunk id ofs | BA_addrglobal id ofs => BA_addrglobal id ofs - | BA_longofwords hi lo => - BA_longofwords (transl_builtin_arg fe hi) (transl_builtin_arg fe lo) + | BA_splitlong hi lo => + BA_splitlong (transl_builtin_arg fe hi) (transl_builtin_arg fe lo) end. (** Translation of a Linear instruction. Prepends the corresponding |