diff options
Diffstat (limited to 'backend/Linear.v')
| -rw-r--r-- | backend/Linear.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/Linear.v b/backend/Linear.v index bdb08b4..3c52436 100644 --- a/backend/Linear.v +++ b/backend/Linear.v @@ -160,7 +160,7 @@ Inductive step: state -> trace -> state -> Prop := E0 (State s f sp b rs' m) | exec_Lsetstack: forall s f sp src sl ofs ty b rs m rs', - rs' = Locmap.set (S sl ofs ty) (rs (R src)) (undef_regs (destroyed_by_op Omove) rs) -> + rs' = Locmap.set (S sl ofs ty) (rs (R src)) (undef_regs (destroyed_by_setstack ty) rs) -> step (State s f sp (Lsetstack src sl ofs ty :: b) rs m) E0 (State s f sp b rs' m) | exec_Lop: |