diff options
Diffstat (limited to 'cfrontend/Cminorgenproof.v')
| -rw-r--r-- | cfrontend/Cminorgenproof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index f94e081..f725662 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -373,9 +373,9 @@ Proof. assert (b0 = b) by congruence. subst. assert (chunk0 = chunk) by congruence. subst. econstructor. eauto. - eapply Mem.load_store_same; eauto. apply val_normalized_has_type; auto. auto. + eapply Mem.load_store_same; eauto. auto. rewrite PTree.gss. reflexivity. - red in H0. rewrite H0. auto. + red in H0. rewrite H0. auto. (* a different variable *) econstructor; eauto. rewrite <- H6. eapply Mem.load_store_other; eauto. |