diff options
Diffstat (limited to 'scheduling/BTL.v')
| -rw-r--r-- | scheduling/BTL.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 8bdafb89..8529010c 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -451,7 +451,7 @@ Inductive match_stackframes: stackframe -> RTL.stackframe -> Prop := | match_stackframe_intro dupmap res f sp pc rs f' pc' (TRANSF: match_function dupmap f f') - (DUPLIC: dupmap!pc' = Some pc) + (DUPLIC: dupmap!pc = Some pc') : match_stackframes (Stackframe res f sp pc rs) (RTL.Stackframe res f' sp pc' rs). Inductive match_states: state -> RTL.state -> Prop := @@ -459,7 +459,7 @@ Inductive match_states: state -> RTL.state -> Prop := dupmap st f sp pc rs m st' f' pc' (STACKS: list_forall2 match_stackframes st st') (TRANSF: match_function dupmap f f') - (DUPLIC: dupmap!pc' = Some pc) + (DUPLIC: dupmap!pc = Some pc') : match_states (State st f sp pc rs m) (RTL.State st' f' sp pc' rs m) | match_states_call st st' f f' args m |