diff options
Diffstat (limited to 'backend/Machabstr2concr.v')
| -rw-r--r-- | backend/Machabstr2concr.v | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/backend/Machabstr2concr.v b/backend/Machabstr2concr.v index 7714f3d5..b766ed0d 100644 --- a/backend/Machabstr2concr.v +++ b/backend/Machabstr2concr.v @@ -231,7 +231,6 @@ Proof. inv H4. assert (Some v1 = Some (Val.load_result (chunk_of_type ty) v')). rewrite <- LOAD1. eapply Mem.load_store_same; eauto. - replace (type_of_chunk (chunk_of_type ty)) with ty. auto. destruct ty; auto. inv H4. rewrite load_result_ty; auto. auto. |