aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Liveness.v
diff options
context:
space:
mode:
Diffstat (limited to 'backend/Liveness.v')
-rw-r--r--backend/Liveness.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/Liveness.v b/backend/Liveness.v
index 16533158..afe11ae6 100644
--- a/backend/Liveness.v
+++ b/backend/Liveness.v
@@ -79,7 +79,7 @@ Definition transfer
reg_list_live args (reg_dead res after)
else
after
- | Iload chunk addr args dst s =>
+ | Iload trap chunk addr args dst s =>
if Regset.mem dst after then
reg_list_live args (reg_dead dst after)
else