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 0f5a1ec9..551462c8 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -36,7 +36,7 @@ Definition slot_valid (s: slot) := match s with | Local ofs ty => 0 <= ofs | Outgoing ofs ty => 14 <= ofs - | Incoming ofs ty => 14 <= ofs /\ ofs + typesize ty <= size_arguments funct.(fn_sig) + | Incoming ofs ty => In (S s) (loc_parameters funct.(fn_sig)) end. Definition slot_writable (s: slot) := |