diff options
Diffstat (limited to 'backend/Lineartyping.v')
| -rw-r--r-- | backend/Lineartyping.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index 2c8de98e..62a0c585 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -59,7 +59,7 @@ Fixpoint wt_builtin_res (ty: typ) (res: builtin_res mreg) : bool := match res with | BR r => subtype ty (mreg_type r) | BR_none => true - | BR_longofwords hi lo => wt_builtin_res Tint hi && wt_builtin_res Tint lo + | BR_splitlong hi lo => wt_builtin_res Tint hi && wt_builtin_res Tint lo end. Definition wt_instr (i: instruction) : bool := |