diff options
Diffstat (limited to 'backend/Tunneling.v')
| -rw-r--r-- | backend/Tunneling.v | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/backend/Tunneling.v b/backend/Tunneling.v index 2f520c61..32d1b595 100644 --- a/backend/Tunneling.v +++ b/backend/Tunneling.v @@ -112,8 +112,6 @@ Definition tunnel_instr (f: LTL.function) (b: instruction) : instruction := Lcall sig ros args res (branch_target f s) | Ltailcall sig ros args => Ltailcall sig ros args - | Lalloc arg res s => - Lalloc arg res (branch_target f s) | Lcond cond args s1 s2 => Lcond cond args (branch_target f s1) (branch_target f s2) | Lreturn or => |