diff options
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/CSE2.v | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/backend/CSE2.v b/backend/CSE2.v index 61abbcdf..87460f90 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -499,7 +499,16 @@ Proof. rewrite PTree.gss. rewrite Regmap.gss. simpl. - replace ( + rewrite args_replace_dst by auto. + assumption. + } + rewrite Regmap.gso by congruence. + unfold sem_reg. + rewrite PTree.gso by congruence. + rewrite Regmap.gso in KILL by congruence. + exact KILL. +Qed. + (* Definition apply_instr instr x := match instr with |